From 70eaae17ede1365220a8b281aba1a337af03ec3c Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 15:47:44 +0800 Subject: [PATCH] chore(Algebra/Homology/ShortComplex/SnakeLemma): remove an erw --- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean index ff5da41877da7e..e21f01884762f4 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean @@ -307,15 +307,11 @@ lemma L₀X₂ToP_comp_φ₁ : S.L₀X₂ToP ≫ S.φ₁ = 0 := by set_option backward.isDefEq.respectTransparency false in lemma L₀_g_δ : S.L₀.g ≫ S.δ = 0 := by - rw [← L₀X₂ToP_comp_pullback_snd, assoc] - erw [S.L₀'_exact.g_desc] - rw [L₀X₂ToP_comp_φ₁_assoc, zero_comp] + rw [← L₀X₂ToP_comp_pullback_snd, assoc, S.snd_δ, L₀X₂ToP_comp_φ₁_assoc, zero_comp] set_option backward.isDefEq.respectTransparency false in lemma δ_L₃_f : S.δ ≫ S.L₃.f = 0 := by - rw [← cancel_epi S.L₀'.g] - erw [S.L₀'_exact.g_desc_assoc] - simp [S.v₂₃.comm₁₂, φ₂] + simp [← cancel_epi S.L₀'.g, δ, S.v₂₃.comm₁₂, φ₂] /-- The short complex `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁`. -/ @[simps]