awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
⊢ Mono.{v_1, u_1} (𝟙 (CokernelCofork.ofπ S.g ⋯).pt)
have dsimp : Mono.{v_1, u_1} (𝟙 S.X₃)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
s : S.Splitting
hp : IsColimit (CokernelCofork.ofπ S.g ⋯)
g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)
hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt
wι : Eq (α := 0 ⟶ (CokernelCofork.ofπ S.g ⋯).pt) (0 ≫ g') 0
⊢ S.RightHomologyData
have have : (hι : IsLimit (KernelFork.ofι 0 wι)) → S.RightHomologyData
Tactic: have hι : IsLimit (KernelFork.ofι 0 wι) := KernelFork.IsLimit.ofMonoOfIsZero _
      (by rw [hg']; dsimp; infer_instance) (isZero_zero _)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ f (S.map F) ≫ F.map s.r = 𝟙 (X₁ (S.map F))
have dsimp : F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
Tactic: dsimp [ShortComplex.map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
have rw : F.map (S.f ≫ s.r) = 𝟙 (F.obj S.X₁)
Tactic: rw [← F.map_comp, f_r, F.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
rw : F.map (S.f ≫ s.r) = 𝟙 (F.obj S.X₁)
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
have rw₁ : F.map (𝟙 S.X₁) = 𝟙 (F.obj S.X₁)
Tactic: rw [← F.map_comp, f_r, F.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
rw : F.map (S.f ≫ s.r) = 𝟙 (F.obj S.X₁)
rw₁ : F.map (𝟙 S.X₁) = 𝟙 (F.obj S.X₁)
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
have rw₂ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj S.X₁) (𝟙 (F.obj S.X₁)) (𝟙 (F.obj S.X₁))
Tactic: rw [← F.map_comp, f_r, F.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ F.map s.s ≫ g (S.map F) = 𝟙 (X₃ (S.map F))
have dsimp : F.map s.s ≫ F.map S.g = 𝟙 (F.obj S.X₃)
Tactic: dsimp [ShortComplex.map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
s : S.Splitting
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
⊢ HAdd.hAdd (α := X₂ (S.map F) ⟶ X₂ (S.map F)) (β := X₂ (S.map F) ⟶ X₂ (S.map F)) (F.map s.r ≫ f (S.map F))
      (g (S.map F) ≫ F.map s.s) =
    𝟙 (X₂ (S.map F))
have dsimp : F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)
Tactic: dsimp [ShortComplex.map]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
have rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
Tactic: rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
have rw₁ : e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
Tactic: rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₁ : e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
have rw₂ : (e.inv ≫ e.hom).τ₁ = 𝟙 S₂.X₁
Tactic: rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₁ : e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₂ : (e.inv ≫ e.hom).τ₁ = 𝟙 S₂.X₁
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
have rw₃ : Hom.τ₁ (𝟙 S₂) = 𝟙 S₂.X₁
Tactic: rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₁ : e.inv.τ₁ ≫ e.hom.τ₁ = 𝟙 S₂.X₁
rw₂ : (e.inv ≫ e.hom).τ₁ = 𝟙 S₂.X₁
rw₃ : Hom.τ₁ (𝟙 S₂) = 𝟙 S₂.X₁
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
have rw₄ : Eq.{v_1 + 1} (α := S₂.X₁ ⟶ S₂.X₁) (𝟙 S₂.X₁) (𝟙 S₂.X₁)
Tactic: rw [← e.inv.comm₁₂_assoc, s.f_r_assoc, ← comp_τ₁, e.inv_hom_id, id_τ₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₃ : e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₃ : e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₄ : (e.inv ≫ e.hom).τ₃ = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₃ : e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₄ : (e.inv ≫ e.hom).τ₃ = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₅ : Hom.τ₃ (𝟙 S₂) = 𝟙 S₂.X₃
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
rw : e.inv.τ₃ ≫ (s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
rw₁ : e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃
rw₂ : e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₃ : e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
rw₄ : (e.inv ≫ e.hom).τ₃ = 𝟙 S₂.X₃
rw₅ : Hom.τ₃ (𝟙 S₂) = 𝟙 S₂.X₃
⊢ (e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂) ≫ S₂.g = 𝟙 S₂.X₃
have rw₆ : Eq.{v_1 + 1} (α := S₂.X₃ ⟶ S₂.X₃) (𝟙 S₂.X₃) (𝟙 S₂.X₃)
Tactic: rw [assoc, assoc, e.hom.comm₂₃, s.s_g_assoc, ← comp_τ₃, e.inv_hom_id, id_τ₃]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂
Tactic: have eq := e.inv.τ₂ ≫= s.id =≫ e.hom.τ₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = e.inv.τ₂ ≫ 𝟙 S₁.X₂ ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have eq₁ : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
Tactic: rw [id_comp, ← comp_τ₂, e.inv_hom_id, id_τ₂] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw : (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₁ : e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₂ : e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₃ : e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₄ : e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₄ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₅ : e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + S₁.g ≫ s.s ≫ e.hom.τ₂)
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₄ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₅ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + S₁.g ≫ s.s ≫ e.hom.τ₂)
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₆ : e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₄ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₅ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + S₁.g ≫ s.s ≫ e.hom.τ₂)
rw₆ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₇ : e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
rw :
  (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₁ :
  e.inv.τ₂ ≫ (s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₂ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂
rw₃ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ ((s.r ≫ S₁.f) ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₄ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + (S₁.g ≫ s.s) ≫ e.hom.τ₂)
rw₅ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ (s.r ≫ S₁.f ≫ e.hom.τ₂ + S₁.g ≫ s.s ≫ e.hom.τ₂)
rw₆ :
  e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
rw₇ :
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂
⊢ (e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁) ≫ S₂.f + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ = 𝟙 S₂.X₂
have rw₈ : e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
  e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂
Tactic: rw [← eq, assoc, assoc, add_comp, assoc, assoc, comp_add,
      e.hom.comm₁₂, e.inv.comm₂₃_assoc]