-- Mathlib/Algebra/Module/SnakeLemma.lean
lemma SnakeLemma.δ_aux (x : K₃) : g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Proof state:
R : Type u_3
inst✝¹² : CommRing R
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_2
N₂ : Type u_1
N₃ : Type ?u.15785
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Tactic:
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]

Result:
case intro
R : Type u_3
inst✝¹² : CommRing R
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_2
N₂ : Type u_1
N₃ : Type ?u.15785
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
d : N₁
hd : g₁ d = i₂ (σ (ι₃ x))
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Proof state:
case intro
R : Type u_3
inst✝¹² : CommRing R
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_2
N₂ : Type u_1
N₃ : Type ?u.15785
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
d : N₁
hd : g₁ d = i₂ (σ (ι₃ x))
⊢ g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))

Tactic:
rw [← hd, ← ρ.comp_apply, hρ, id_eq]

Result:
no goals

Proof state:
R : Type u_3
inst✝¹² : CommRing R
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_2
N₂ : Type u_1
N₃ : Type ?u.15785
inst✝¹¹ : AddCommGroup M₂
inst✝¹⁰ : Module R M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₃
inst✝⁷ : AddCommGroup N₁
inst✝⁶ : Module R N₁
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₃
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_6
inst✝¹ : AddCommGroup K₃
inst✝ : Module R K₃
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
x : K₃
⊢ i₂ (σ (ι₃ x)) ∈ range g₁

Tactic:
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]

Result:
no goals