English
A restatement emphasizing the injectivity conclusion under analogous conditions.
Русский
Повторение формулировки инъективности в аналогичных условиях.
LaTeX
$$injective_of_surjective_of_injective_of_injective hi1 hi2 hi4 : Function.Injective i3$$
Lean4
/-- One four lemma in terms of (additive) groups. For a diagram explaining the variables,
see the module docstring. -/
theorem injective_of_surjective_of_injective_of_injective (hi₁ : Function.Surjective i₁) (hi₂ : Function.Injective i₂)
(hi₄ : Function.Injective i₄) : Function.Injective i₃ :=
by
rw [injective_iff_map_eq_zero]
intro m hm
obtain ⟨x, rfl⟩ :=
(hf₂ m).mp <| by
suffices h : i₄ (f₃ m) = 0 by rwa [map_eq_zero_iff _ hi₄] at h
simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]
obtain ⟨y, hy⟩ := (hg₁ _).mp <| by rwa [show g₂ (i₂ x) = i₃ (f₂ x) by simpa using DFunLike.congr_fun hc₂ x]
obtain ⟨a, rfl⟩ := hi₁ y
rw [show g₁ (i₁ a) = i₂ (f₁ a) by simpa using DFunLike.congr_fun hc₁ a] at hy
apply hi₂ at hy
subst hy
rw [hf₁.apply_apply_eq_zero]
