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₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₂.τ₁ + -(S₁.f ≫ h.h₁ + h.h₀) = -S₁.f ≫ h.h₁ + -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 : Homotopy φ₁ φ₂
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 + (-φ₂).τ₂

Tactic:
rw [neg_τ₂, neg_τ₂, h.comm₂, neg_add_rev, comp_neg, neg_comp]

Premises used: neg_add_rev, CategoryTheory.Preadditive.comp_neg, CategoryTheory.ShortComplex.neg_τ₂, CategoryTheory.Preadditive.neg_comp, 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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₂.τ₂ + -(S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f) = -S₁.g ≫ h.h₂ + -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 : Homotopy φ₁ φ₂
rw : -(h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.h₃ + -h.h₂ ≫ S₂.g + -φ₂.τ₃
⊢ (-φ₁).τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃

Tactic:
rw [neg_τ₃, neg_τ₃, h.comm₃, neg_comp]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.Preadditive.neg_comp, CategoryTheory.ShortComplex.neg_τ₃
-- 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 : Homotopy φ₁ φ₂
⊢ -(h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.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₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
rw :
  S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
⊢ φ₁.τ₁ = S₁.f ≫ (h₁₂.h₁ + h₂₃.h₁) + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁

Tactic:
rw [h₁₂.comm₁, h₂₃.comm₁, comp_add]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.Preadditive.comp_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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + 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₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
rw :
  S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + h₂₃.h₁ ≫ S₂.f) + φ₃.τ₂
⊢ φ₁.τ₂ = S₁.g ≫ (h₁₂.h₂ + h₂₃.h₂) + (h₁₂.h₁ + h₂₃.h₁) ≫ S₂.f + φ₃.τ₂

Tactic:
rw [h₁₂.comm₂, h₂₃.comm₂, comp_add, add_comp]

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, 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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.g ≫ h₁₂.h₂ + h₁₂.h₁ ≫ S₂.f + (S₁.g ≫ h₂₃.h₂ + h₂₃.h₁ ≫ S₂.f + φ₃.τ₂) =
    S₁.g ≫ h₁₂.h₂ + S₁.g ≫ h₂₃.h₂ + (h₁₂.h₁ ≫ S₂.f + 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₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
rw :
  h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + h₂₃.h₂ ≫ S₂.g) + φ₃.τ₃
⊢ φ₁.τ₃ = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ + h₂₃.h₂) ≫ S₂.g + φ₃.τ₃

Tactic:
rw [h₁₂.comm₃, h₂₃.comm₃, add_comp]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.Preadditive.add_comp
-- 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₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ h₁₂.h₃ + h₁₂.h₂ ≫ S₂.g + (h₂₃.h₃ + h₂₃.h₂ ≫ S₂.g + φ₃.τ₃) = h₁₂.h₃ + h₂₃.h₃ + (h₁₂.h₂ ≫ S₂.g + 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ + S₁.f ≫ h'.h₁ + (h.h₀ + h'.h₀) + (φ₂.τ₁ + φ₄.τ₁)
⊢ (φ₁ + φ₃).τ₁ = S₁.f ≫ (h.h₁ + h'.h₁) + (h.h₀ + h'.h₀) + (φ₂ + φ₄).τ₁

Tactic:
rw [add_τ₁, add_τ₁, h.comm₁, h'.comm₁, comp_add]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.Preadditive.comp_add, CategoryTheory.ShortComplex.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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ + (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ + S₁.f ≫ h'.h₁ + (h.h₀ + 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + h'.h₁ ≫ S₂.f) + (φ₂.τ₂ + φ₄.τ₂)
⊢ (φ₁ + φ₃).τ₂ = S₁.g ≫ (h.h₂ + h'.h₂) + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂ + φ₄).τ₂

Tactic:
rw [add_τ₂, add_τ₂, h.comm₂, h'.comm₂, comp_add, add_comp]

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.ShortComplex.add_τ₂, CategoryTheory.Preadditive.comp_add, 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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ + S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f + 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + h'.h₂ ≫ S₂.g) + (φ₂.τ₃ + φ₄.τ₃)
⊢ (φ₁ + φ₃).τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂ + φ₄).τ₃

Tactic:
rw [add_τ₃, add_τ₃, h.comm₃, h'.comm₃, add_comp]

Premises used: CategoryTheory.ShortComplex.add_τ₃, CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.Preadditive.add_comp
-- 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ + (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ + h'.h₃ + (h.h₂ ≫ S₂.g + 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ - S₁.f ≫ h'.h₁ + (h.h₀ - h'.h₀) + (φ₂.τ₁ - φ₄.τ₁)
⊢ (φ₁ - φ₃).τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂ - φ₄).τ₁

Tactic:
rw [sub_τ₁, sub_τ₁, h.comm₁, h'.comm₁, comp_sub]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.ShortComplex.sub_τ₁, CategoryTheory.Preadditive.comp_sub
-- 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ - (S₁.f ≫ h'.h₁ + h'.h₀ + φ₄.τ₁) =
    S₁.f ≫ h.h₁ - S₁.f ≫ h'.h₁ + (h.h₀ - 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - h'.h₁ ≫ S₂.f) + (φ₂.τ₂ - φ₄.τ₂)
⊢ (φ₁ - φ₃).τ₂ = S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂ - φ₄).τ₂

Tactic:
rw [sub_τ₂, sub_τ₂, h.comm₂, h'.comm₂, comp_sub, sub_comp]

Premises used: CategoryTheory.ShortComplex.sub_τ₂, CategoryTheory.ShortComplex.Homotopy.comm₂, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
rw :
  h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - h'.h₂ ≫ S₂.g) + (φ₂.τ₃ - φ₄.τ₃)
⊢ (φ₁ - φ₃).τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃

Tactic:
rw [sub_τ₃, sub_τ₃, h.comm₃, h'.comm₃, sub_comp]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.ShortComplex.sub_τ₃, CategoryTheory.Preadditive.sub_comp
-- 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 : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - 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 : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₂ ≫ S₁.g ≫ h.h₃ = 0
rw₁ : Eq (α := S₃.X₂ ⟶ S₂.X₃) (ψ.τ₂ ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S₃.X₂ ⟶ S₂.X₃) 0 0
⊢ S₃.g ≫ ψ.τ₃ ≫ h.h₃ = 0

Tactic:
rw [← ψ.comm₂₃_assoc, h.g_h₃, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.ShortComplex.Homotopy.g_h₃, CategoryTheory.ShortComplex.Hom.comm₂₃_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 : Homotopy φ₁ φ₂
ψ : S₃ ⟶ S₁
rw : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁
rw₁ : ψ.τ₁ ≫ φ₁.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₂ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₃ : ψ.τ₁ ≫ (S₁.f ≫ h.h₁ + h.h₀) + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₄ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + ψ.τ₁ ≫ φ₂.τ₁
rw₅ : ψ.τ₁ ≫ S₁.f ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
rw₆ rw₇ : S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀
⊢ (ψ ≫ φ₁).τ₁ = S₃.f ≫ ψ.τ₂ ≫ h.h₁ + ψ.τ₁ ≫ h.h₀ + (ψ ≫ φ₂).τ₁

Tactic:
rw [comp_τ₁, comp_τ₁, h.comm₁, comp_add, comp_add, add_left_inj, ψ.comm₁₂_assoc]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.ShortComplex.comp_τ₁, CategoryTheory.ShortComplex.Hom.comm₁₂_assoc, add_left_inj, CategoryTheory.Preadditive.comp_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₂ 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₆ 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 + (ψ ≫ φ₂).τ₂

Tactic:
rw [comp_τ₂, comp_τ₂, h.comm₂, comp_add, comp_add, assoc, ψ.comm₂₃_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.Preadditive.comp_add, CategoryTheory.ShortComplex.Homotopy.comm₂, CategoryTheory.ShortComplex.Hom.comm₂₃_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 : 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₅ rw₆ : ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃ = ψ.τ₃ ≫ h.h₃ + ψ.τ₃ ≫ h.h₂ ≫ S₂.g + ψ.τ₃ ≫ φ₂.τ₃
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃

Tactic:
rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.ShortComplex.comp_τ₃, CategoryTheory.Preadditive.comp_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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
ψ : S₂ ⟶ S₃
rw : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁
rw₁ : φ₁.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₂ : (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₃ : (S₁.f ≫ h.h₁ + h.h₀) ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₄ : (S₁.f ≫ h.h₁) ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
rw₅ rw₆ : S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + φ₂.τ₁ ≫ ψ.τ₁
⊢ (φ₁ ≫ ψ).τ₁ = S₁.f ≫ h.h₁ ≫ ψ.τ₁ + h.h₀ ≫ ψ.τ₁ + (φ₂ ≫ ψ).τ₁

Tactic:
rw [comp_τ₁, comp_τ₁, h.comm₁, add_comp, add_comp, assoc]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.comp_τ₁, CategoryTheory.Preadditive.add_comp
-- 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 : 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 + φ₂.τ₂ ≫ ψ.τ₂
rw₈ 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 + (φ₂ ≫ ψ).τ₂

Tactic:
rw [comp_τ₂, comp_τ₂, h.comm₂, add_comp, add_comp, assoc, assoc, assoc, ψ.comm₁₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Hom.comm₁₂, CategoryTheory.ShortComplex.comp_τ₂, CategoryTheory.Preadditive.add_comp, 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₂ 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 + φ₂.τ₃ ≫ ψ.τ₃
rw₇ rw₈ : h.h₃ ≫ ψ.τ₃ + h.h₂ ≫ S₂.g ≫ ψ.τ₃ + φ₂.τ₃ ≫ ψ.τ₃ = 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₂₃]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.Homotopy.comm₃, CategoryTheory.Preadditive.add_comp, CategoryTheory.ShortComplex.Hom.comm₂₃, CategoryTheory.ShortComplex.comp_τ₃
-- 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 : Homotopy φ₁ φ₂
dsimp : φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
⊢ (opMap φ₁).τ₁.unop = (S₂.op.f ≫ h.h₂.op + h.h₃.op + (opMap φ₂).τ₁).unop

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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
rw : 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₂ 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 : Homotopy φ₁ φ₂
dsimp : φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
⊢ (opMap φ₁).τ₂.unop = (S₂.op.g ≫ h.h₁.op + h.h₂.op ≫ S₁.op.f + (opMap φ₂).τ₂).unop

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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
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₁ 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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
dsimp : φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
⊢ (opMap φ₁).τ₃.unop = (h.h₀.op + h.h₁.op ≫ S₁.op.g + (opMap φ₂).τ₃).unop

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₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
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₁ 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₁_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₂.g + h.h₃ + φ₂.τ₃
⊢ (unopMap φ₁).τ₁.op = (S₂.unop.f ≫ h.h₂.unop + h.h₃.unop + (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 : 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₁_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₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃

Tactic:
abel