awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
dsimp : φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
⊢ (unopMap φ₁).τ₂.op = (S₂.unop.g ≫ h.h₁.unop + h.h₂.unop ≫ S₁.unop.f + (unopMap φ₂).τ₂).op

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
rw : S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
⊢ φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
rw [h.comm₂]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
dsimp : φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
⊢ (unopMap φ₁).τ₃.op = (h.h₀.unop + h.h₁.unop ≫ S₁.unop.g + (unopMap φ₂).τ₃).op

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
rw : S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
rw [h.comm₁]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₂) φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₃ ⋯).τ₂
h₃ : φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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.h₀ + S₁.f ≫ h.h₁)
⊢ φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
rw [h.comm₁]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
⊢ φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)
⊢ φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Tactic:
rw [h.comm₂]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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.h₂ ≫ S₂.g + h.h₃)
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)
⊢ φ₁.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Tactic:
rw [h.comm₃]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₃
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
rw : h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0

Tactic:
rw [nullHomotopic_τ₁, zero_τ₁, add_zero]

Premises used: CategoryTheory.ShortComplex.nullHomotopic_τ₁, CategoryTheory.ShortComplex.zero_τ₁, add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
rw : h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0

Tactic:
rw [nullHomotopic_τ₂, zero_τ₂, add_zero]

Premises used: CategoryTheory.ShortComplex.nullHomotopic_τ₂, add_zero, CategoryTheory.ShortComplex.zero_τ₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
⊢ h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
rw : h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = h₃ + h₂ ≫ S₂.g + Hom.τ₃ 0

Tactic:
rw [nullHomotopic_τ₃, zero_τ₃, add_zero]

Premises used: CategoryTheory.ShortComplex.zero_τ₃, CategoryTheory.ShortComplex.nullHomotopic_τ₃, add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
⊢ h₂ ≫ S₂.g + h₃ = h₃ + h₂ ≫ S₂.g

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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) ≫ S₂.g = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
rw₁₂ rw₁₃ : Eq.{v_1 + 1} (α := S₁.X₁ ⟶ S₂.X₂) 0 0
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.liftK_i, CategoryTheory.ShortComplex.nullHomotopic_τ₁, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Preadditive.add_comp, CategoryTheory.ShortComplex.LeftHomologyData.f'_i_assoc, right_eq_add, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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 rw₁ : H₁.i ≫ h₁ ≫ S₂.f = H₁.i ≫ h₁ ≫ S₂.f
⊢ H₁.i ≫ h₁ ≫ S₂.f = (H₁.i ≫ h₁) ≫ S₂.f

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
rw₁ rw₂ : Eq.{v_1 + 1} (α := H₁.K ⟶ H₂.H) 0 0
⊢ H₁.π ≫ 0 = H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ ≫ H₂.π

Tactic:
rw [H₂.liftK_π_eq_zero_of_boundary (H₁.i ≫ h₁ ≫ S₂.f) (H₁.i ≫ h₁) (by rw [assoc]), comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.LeftHomologyData.liftK_π_eq_zero_of_boundary, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.f, CategoryTheory.ShortComplex.LeftHomologyData.i
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
⊢ S₁.f ≫ S₁.g ≫ h₂ ≫ H₂.p = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₃
rw₈ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g + 0
rw₉ rw₁₀ : S₁.g ≫ h₂ ≫ S₂.g = S₁.g ≫ h₂ ≫ S₂.g
⊢ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯ ≫ H₂.g' = 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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, CategoryTheory.ShortComplex.RightHomologyData.p_descQ_assoc, CategoryTheory.ShortComplex.nullHomotopic_τ₃, CategoryTheory.Preadditive.comp_add, add_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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 : Eq (α := H₁.H ⟶ H₂.Q) (0 ≫ H₂.ι) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := H₁.H ⟶ H₂.Q) 0 0
⊢ 0 ≫ H₂.ι = H₁.ι ≫ H₁.descQ (S₁.g ≫ h₂ ≫ H₂.p) ⋯

Tactic:
rw [H₁.ι_descQ_eq_zero_of_boundary (S₁.g ≫ h₂ ≫ H₂.p) (h₂ ≫ H₂.p) rfl, zero_comp]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp, CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary, CategoryTheory.ShortComplex.g, rfl, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
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
⊢ leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Tactic:
(LeftHomologyMapData.ofNullHomotopic H₁ H₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).leftHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.ofNullHomotopic, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
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
⊢ rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Tactic:
(RightHomologyMapData.ofNullHomotopic H₁ H₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).rightHomologyMap'_eq

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
H₁ : S₁.HomologyData
H₂ : S₂.HomologyData
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
⊢ homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
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
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃)) 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
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
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃)) 0

Tactic:
apply rightHomologyMap'_nullHomotopic

Premises used: CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
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
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃)) 0

Tactic:
apply homologyMap'_nullHomotopic

Premises used: CategoryTheory.ShortComplex.homologyMap'_nullHomotopic
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
rw : leftHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
rw₁ :
  leftHomologyMap' φ₂ h₁ h₂ + leftHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    leftHomologyMap' φ₂ h₁ h₂
rw₂ : leftHomologyMap' φ₂ h₁ h₂ + 0 = leftHomologyMap' φ₂ h₁ h₂
rw₃ rw₄ : leftHomologyMap' φ₂ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂
⊢ leftHomologyMap' φ₁ h₁ h₂ = leftHomologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, leftHomologyMap'_add, leftHomologyMap'_nullHomotopic, add_zero]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic, CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic, add_zero, CategoryTheory.ShortComplex.leftHomologyMap'_add
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
rw : rightHomologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
rw₁ :
  rightHomologyMap' φ₂ h₁ h₂ + rightHomologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ =
    rightHomologyMap' φ₂ h₁ h₂
rw₂ : rightHomologyMap' φ₂ h₁ h₂ + 0 = rightHomologyMap' φ₂ h₁ h₂
rw₃ rw₄ : rightHomologyMap' φ₂ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂
⊢ rightHomologyMap' φ₁ h₁ h₂ = rightHomologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, rightHomologyMap'_add, rightHomologyMap'_nullHomotopic, add_zero]

Premises used: CategoryTheory.ShortComplex.rightHomologyMap'_add, CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic, CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic, add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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₁.HomologyData
h₂ : S₂.HomologyData
rw : homologyMap' (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
rw₁ : homologyMap' φ₂ h₁ h₂ + homologyMap' (S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯) h₁ h₂ = homologyMap' φ₂ h₁ h₂
rw₂ : homologyMap' φ₂ h₁ h₂ + 0 = homologyMap' φ₂ h₁ h₂
rw₃ rw₄ : homologyMap' φ₂ h₁ h₂ = homologyMap' φ₂ h₁ h₂
⊢ homologyMap' φ₁ h₁ h₂ = homologyMap' φ₂ h₁ h₂

Tactic:
rw [h.eq_add_nullHomotopic, homologyMap'_add, homologyMap'_nullHomotopic, add_zero]

Premises used: CategoryTheory.ShortComplex.homologyMap'_nullHomotopic, CategoryTheory.ShortComplex.homologyMap'_add, CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic, add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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 φ₁ φ₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ₁) (leftHomologyMap φ₂)

Tactic:
h.leftHomologyMap'_congr _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, CategoryTheory.ShortComplex.Homotopy.leftHomologyMap'_congr
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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 φ₁ φ₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ₁) (rightHomologyMap φ₂)

Tactic:
h.rightHomologyMap'_congr _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr, CategoryTheory.ShortComplex.rightHomologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
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 φ₁ φ₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap φ₁) (homologyMap φ₂)

Tactic:
h.homologyMap'_congr _ _

Premises used: CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap