English
In the Snake Lemma configuration, the auxiliary equality holds: g1(ρ(i2(σ(ι3 x)))) = i2(σ(ι3 x)) for x ∈ K3.
Русский
В конфигурации Змеиного леммы выполняется вспомогательное равенство: g1(ρ(i2(σ(ι3 x)))) = i2(σ(ι3 x)) для x ∈ K3.
LaTeX
$$$g_1\\bigl(\\rho\\bigl(i_2(\\sigma(\\iota_3(x)))\\bigr)\\bigr) = i_2\\bigl(\\sigma(\\iota_3(x))\\bigr)$$$
Lean4
theorem δ_aux (x : K₃) : g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x)) :=
by
obtain ⟨d, hd⟩ : i₂ (σ (ι₃ x)) ∈ range g₁ := by
rw [← hg.linearMap_ker_eq, mem_ker, show g₂ (i₂ _) = i₃ (f₂ _) from DFunLike.congr_fun h₂ _, ←
@comp_apply _ _ _ f₂ σ, hσ, id_eq, ← i₃.comp_apply, hι₃.linearMap_comp_eq_zero, zero_apply]
rw [← hd, ← ρ.comp_apply, hρ, id_eq]
