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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₄ :
  (S₁.g ≫ h.h₂) ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₅ :
  S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₆ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₄ :
  (S₁.g ≫ h.h₂) ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₅ :
  S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₆ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₇ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ ψ.τ₁ ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
rw₁ : φ₁.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₂ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂) ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₃ : (S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₄ :
  (S₁.g ≫ h.h₂) ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₅ :
  S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ S₂.f) ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₆ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
rw₇ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ ψ.τ₁ ≫ S₃.f + φ₂.τ₂ ≫ ψ.τ₂
⊢ (φ₁ ≫ ψ).τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + (h.h₁ ≫ ψ.τ₁) ≫ S₃.f + (φ₂ ≫ ψ).τ₂
have rw₈ : S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂ = S₁.g ≫ h.h₂ ≫ ψ.τ₂ + h.h₁ ≫ S₂.f ≫ ψ.τ₂ + φ₂.τ₂ ≫ ψ.τ₂
Tactic: rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₃ : (h.h₃ + h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₃ : (h.h₃ + h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₄ : h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₃ : (h.h₃ + h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₄ : h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₅ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₃ : (h.h₃ + h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₄ : h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₅ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₆ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ ψ.τ₂ ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
rw₁ : φ₁.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₂ : (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₃ : (h.h₃ + h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₄ : h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ S₂.g) ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₅ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
rw₆ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ ψ.τ₂ ≫ S₃.g + φ₂.τ₃ ≫ ψ.τ₃
⊢ (φ₁ ≫ ψ).τ₃ = h.h₃ ≫ ψ.τ₃ + (h.h₂ ≫ ψ.τ₂) ≫ S₃.g + (φ₂ ≫ ψ).τ₃
have rw₇ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃
Tactic: rw [comp_τ₃, comp_τ₃, h.comm₃, add_comp, add_comp, assoc, assoc, ψ.comm₂₃]
-- 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 : Homotopy φ₁ φ₂
⊢ (opMap φ₁).τ₁.unop = (S₂.op.f ≫ h.h₂.op + h.h₃.op + (opMap φ₂).τ₁).unop
have dsimp : φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
Tactic: dsimp
-- 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 : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
have rw : h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
Tactic: rw [h.comm₃]
-- 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 : Homotopy φ₁ φ₂
⊢ (opMap φ₁).τ₂.unop = (S₂.op.g ≫ h.h₁.op + h.h₂.op ≫ S₁.op.f + (opMap φ₂).τ₂).unop
have dsimp : φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Tactic: dsimp
-- 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 : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
have rw : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Tactic: rw [h.comm₂]
-- 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 : Homotopy φ₁ φ₂
⊢ (opMap φ₁).τ₃.unop = (h.h₀.op + h.h₁.op ≫ S₁.op.g + (opMap φ₂).τ₃).unop
have dsimp : φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Tactic: dsimp
-- 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 : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
have rw : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Tactic: rw [h.comm₁]
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ (unopMap φ₁).τ₁.op = (S₂.unop.f ≫ h.h₂.unop + h.h₃.unop + (unopMap φ₂).τ₁).op
have dsimp : φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
Tactic: dsimp
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
have rw : h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
Tactic: rw [h.comm₃]
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ (unopMap φ₁).τ₂.op = (S₂.unop.g ≫ h.h₁.unop + h.h₂.unop ≫ S₁.unop.f + (unopMap φ₂).τ₂).op
have dsimp : φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Tactic: dsimp
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
have rw : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
Tactic: rw [h.comm₂]
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ (unopMap φ₁).τ₃.op = (h.h₀.unop + h.h₁.unop ≫ S₁.unop.g + (unopMap φ₂).τ₃).op
have dsimp : φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Tactic: dsimp
-- 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₁_1 S₂_1 S₃ : ShortComplex.{v_1, u_1} C
φ₁_1 φ₂_1 φ₃ φ₄ : S₁_1 ⟶ S₂_1
S₁ S₂ : ShortComplex.{v_1, u_1} Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy.{v_1, u_1} (C := Cᵒᵖ) (S₁ := S₁) (S₂ := S₂) φ₁ φ₂
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
have rw : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Tactic: rw [h.comm₁]
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
have h₁ : φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry).τ₁
Tactic: ext
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
have h₂ : φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry).τ₂
Tactic: ext
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h₁ : φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁
h₂ : φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯
have h₃ : φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ sorry h.h₁ h.h₂ h.h₃ sorry).τ₃
Tactic: ext
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁
have h₁ : φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
Tactic: dsimp
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
have h₁ : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
Tactic: rw [h.comm₁]
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂
have h₂ : φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
Tactic: dsimp
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
have h₂ : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
Tactic: rw [h.comm₂]
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃
have h₃ : φ₁.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)
Tactic: dsimp
-- 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₂ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)
have h₃ : h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)
Tactic: rw [h.comm₃]
-- 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₁.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
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0
have rw : h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀
Tactic: rw [nullHomotopic_τ₁, zero_τ₁, 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₁.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
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0
have rw : h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f
Tactic: rw [nullHomotopic_τ₂, zero_τ₂, 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₁.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
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = h₃ + h₂ ≫ S₂.g + Hom.τ₃ 0
have rw : h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g
Tactic: rw [nullHomotopic_τ₃, zero_τ₃, 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₁.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₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw : (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) sorry) ≫ H₂.i = ((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
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₁ : H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) sorry ≫ H₂.i = ((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
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'
have rw₂ : H₁.f' ≫ H₁.i ≫ 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]