-- Mathlib/Algebra/Module/SnakeLemma.lean
/--
Suppose we have an exact commutative diagram
```
        K₂ -F-→ K₃
        |       |
        ι₂      ι₃
        ↓       ↓
M₁ -f₁→ M₂ -f₂→ M₃
|       |       |
i₁      i₂      i₃
↓       ↓       ↓
N₁ -g₁→ N₂ -g₂→ N₃
|
π₁
↓
C₁

```
such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
(set-theoretic) retraction `ρ`, and `ι₃` is injective, then `K₂ -F→ K₂ -δ→ C₁` is exact.
-/
lemma SnakeLemma.exact_δ_right (F : K₂ →ₗ[R] K₃) (hF : f₂.comp ι₂ = ι₃.comp F)
    (h : Injective ι₃) :
    Exact F (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Proof state:
case mpr.intro
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_7
M₂ : Type u_5
M₃ : Type u_4
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_2
K₃ : Type u_3
C₁ : Type u_6
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
y : K₂
⊢ (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) (F y) = 0

Tactic:
exact (δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ (ι₂ y) congr($hF y)
  _ (by rw [map_zero, hι₂.apply_apply_eq_zero])).trans π₁.map_zero

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_7
M₂ : Type u_5
M₃ : Type u_4
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
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₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₂ : Type u_2
K₃ : Type u_3
C₁ : Type u_6
inst✝⁵ : AddCommGroup K₂
inst✝⁴ : Module R K₂
inst✝³ : AddCommGroup K₃
inst✝² : Module R K₃
inst✝¹ : AddCommGroup C₁
inst✝ : Module R C₁
ι₂ : K₂ →ₗ[R] M₂
hι₂ : Exact ⇑ι₂ ⇑i₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
F : K₂ →ₗ[R] K₃
hF : f₂ ∘ₗ ι₂ = ι₃ ∘ₗ F
h : Injective ⇑ι₃
H₁ : ∀ (x : M₃), f₂ (σ x) = x
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : K₃
H : (δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁) x = 0
y : M₁
hy : i₁ y = ρ (i₂ (σ (ι₃ x)))
k : K₂
hk : ι₂ k = σ (ι₃ x) - f₁ y
⊢ ι₃ (F k) = ι₃ x

Tactic:
rw [← ι₃.comp_apply, ← hF, f₂.comp_apply, hk, map_sub, H₁, hf.apply_apply_eq_zero, sub_zero]

Result:
no goals