awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₇ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₇ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₈ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + (S₁.f ≫ h₁) ≫ H₂.f' ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₇ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₈ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + (S₁.f ≫ h₁) ≫ H₂.f' ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₉ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + S₁.f ≫ h₁ ≫ H₂.f' ≫ H₂.i
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₇ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₈ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + (S₁.f ≫ h₁) ≫ H₂.f' ≫ H₂.i
rw₉ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + S₁.f ≫ h₁ ≫ H₂.f' ≫ H₂.i
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₁₀ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ S₂.f + S₁.f ≫ h₁ ≫ S₂.f
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₂ : H₁.f' ≫ H₁.i ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₃ : S₁.f ≫ h₁ ≫ S₂.f = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
rw₄ : S₁.f ≫ h₁ ≫ S₂.f = ((h₀ + S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₅ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f' + (S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₆ : S₁.f ≫ h₁ ≫ S₂.f = (h₀ ≫ H₂.f') ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₇ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + ((S₁.f ≫ h₁) ≫ H₂.f') ≫ H₂.i
rw₈ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + (S₁.f ≫ h₁) ≫ H₂.f' ≫ H₂.i
rw₉ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ H₂.f' ≫ H₂.i + S₁.f ≫ h₁ ≫ H₂.f' ≫ H₂.i
rw₁₀ : S₁.f ≫ h₁ ≫ S₂.f = h₀ ≫ S₂.f + S₁.f ≫ h₁ ≫ S₂.f
rw₁₁ : h₀ ≫ S₂.f = 0
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₁₂ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
Tactic: rw [← cancel_mono H₂.i, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
      nullHomotopic_τ₁, add_comp, add_comp, assoc, assoc, assoc, LeftHomologyData.f'_i,
      right_eq_add, h₀_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.i ≫ h₁ ≫ S₂.f = (H₁.i ≫ h₁) ≫ S₂.f
have rw : H₁.i ≫ h₁ ≫ S₂.f = H₁.i ≫ h₁ ≫ S₂.f
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.π ≫ 0 = H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.π
have rw : Eq (α := H₁.K ⟶ H₂.H) (H₁.π ≫ 0) 0
Tactic: rw [H₂.liftK_π_eq_zero_of_boundary (H₁.i ≫ h₁ ≫ S₂.f) (H₁.i ≫ h₁) (by rw [assoc]), comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : Eq (α := H₁.K ⟶ H₂.H) (H₁.π ≫ 0) 0
⊢ H₁.π ≫ 0 = H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.π
have rw₁ : Eq.{v_1 + 1} (α := H₁.K ⟶ H₂.H) 0 0
Tactic: rw [H₂.liftK_π_eq_zero_of_boundary (H₁.i ≫ h₁ ≫ S₂.f) (H₁.i ≫ h₁) (by rw [assoc]), comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) sorry ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₅ : S₁.g ≫ (h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₅ : S₁.g ≫ (h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₆ : S₁.g ≫ h₂ ≫ H₂.p ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₅ : S₁.g ≫ (h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₆ : S₁.g ≫ h₂ ≫ H₂.p ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₇ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Preadditive (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.RightHomologyData
H₂ : S₂.RightHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
rw : H₁.p ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₁ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = H₁.p ≫ H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₂ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
rw₃ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ (h₂ ≫ S₂.g + h₃)
rw₄ : (S₁.g ≫ h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₅ : S₁.g ≫ (h₂ ≫ H₂.p) ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₆ : S₁.g ≫ h₂ ≫ H₂.p ≫ H₂.g' = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
rw₇ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + S₁.g ≫ h₃
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = H₁.g' ≫ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃
have rw₈ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + 0
Tactic: rw [← cancel_epi H₁.p, RightHomologyData.p_descQ_assoc, RightHomologyData.p_g'_assoc,
      nullHomotopic_τ₃, comp_add, assoc, assoc, RightHomologyData.p_g', g_h₃, add_zero]