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]