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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Tactic:
simp only [γ.cyclesMap'_eq, γ.neg.cyclesMap'_eq, LeftHomologyMapData.neg_φK]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.neg, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_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
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
have :
  ∀ (γ : LeftHomologyMapData φ h₁ h₂),
    leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
have :
  ∀ (γ' : LeftHomologyMapData φ' h₁ h₂),
    leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default
-- 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ leftHomologyMap' (φ + φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ + leftHomologyMap' φ' h₁ h₂

Tactic:
simp only [γ.leftHomologyMap'_eq, γ'.leftHomologyMap'_eq,
    (γ.add γ').leftHomologyMap'_eq, LeftHomologyMapData.add_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.add, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH, 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
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
have : ∀ (γ : LeftHomologyMapData φ h₁ h₂), cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
have : ∀ (γ' : LeftHomologyMapData φ' h₁ h₂), cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default
-- 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
simp only [γ.cyclesMap'_eq, γ'.cyclesMap'_eq,
    (γ.add γ').cyclesMap'_eq, LeftHomologyMapData.add_φK]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.add, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_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
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ - leftHomologyMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, leftHomologyMap'_add, leftHomologyMap'_neg]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_neg, sub_eq_add_neg, 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₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (φ - φ') h₁ h₂ = cyclesMap' φ h₁ h₂ - cyclesMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, cyclesMap'_add, cyclesMap'_neg]

Premises used: sub_eq_add_neg, CategoryTheory.ShortComplex.cyclesMap'_add, CategoryTheory.ShortComplex.cyclesMap'_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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap (-φ)) (-leftHomologyMap φ)

Tactic:
leftHomologyMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomologyMap'_neg, CategoryTheory.ShortComplex.leftHomology
-- 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₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ Eq (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap (-φ)) (-cyclesMap φ)

Tactic:
cyclesMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cyclesMap'_neg, CategoryTheory.ShortComplex.cycles
-- 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₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ leftHomologyMap (φ + φ') = HAdd.hAdd (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ) (leftHomologyMap φ')

Tactic:
leftHomologyMap'_add _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology, 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₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ cyclesMap (φ + φ') = HAdd.hAdd (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (cyclesMap φ')

Tactic:
cyclesMap'_add _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cyclesMap'_add, CategoryTheory.ShortComplex.cycles
-- 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₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ leftHomologyMap (φ - φ') = HSub.hSub (α := S₁.leftHomology ⟶ S₂.leftHomology) (leftHomologyMap φ) (leftHomologyMap φ')

Tactic:
leftHomologyMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_sub, CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.leftHomology
-- 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₂
inst_2 : S₁.HasLeftHomology
inst_3 : S₂.HasLeftHomology
⊢ cyclesMap (φ - φ') = HSub.hSub (α := S₁.cycles ⟶ S₂.cycles) (cyclesMap φ) (cyclesMap φ')

Tactic:
cyclesMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap'_sub, CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.cycles
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ rightHomologyMap' (-φ) h₁ h₂ = -rightHomologyMap' φ h₁ h₂

Tactic:
simp only [γ.rightHomologyMap'_eq, γ.neg.rightHomologyMap'_eq, RightHomologyMapData.neg_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ.neg.opcyclesMap'_eq, RightHomologyMapData.neg_φQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.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₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
have :
  ∀ (γ : RightHomologyMapData φ h₁ h₂),
    rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
have :
  ∀ (γ' : RightHomologyMapData φ' h₁ h₂),
    rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
have γ' : RightHomologyMapData φ' h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ rightHomologyMap' (φ + φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ + rightHomologyMap' φ' h₁ h₂

Tactic:
simp only [γ.rightHomologyMap'_eq, γ'.rightHomologyMap'_eq,
    (γ.add γ').rightHomologyMap'_eq, RightHomologyMapData.add_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.add, CategoryTheory.ShortComplex.RightHomologyMapData.add_φH
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
have : ∀ (γ : RightHomologyMapData φ h₁ h₂), opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
have :
  ∀ (γ' : RightHomologyMapData φ' h₁ h₂), opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
have γ' : RightHomologyMapData φ' h₁ h₂ := default
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ'.opcyclesMap'_eq,
    (γ.add γ').opcyclesMap'_eq, RightHomologyMapData.add_φQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.add, CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ
-- 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₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (φ - φ') h₁ h₂ = rightHomologyMap' φ h₁ h₂ - rightHomologyMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, rightHomologyMap'_add, rightHomologyMap'_neg]

Premises used: sub_eq_add_neg, CategoryTheory.ShortComplex.rightHomologyMap'_add, CategoryTheory.ShortComplex.rightHomologyMap'_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₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (φ - φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ - opcyclesMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, opcyclesMap'_add, opcyclesMap'_neg]

Premises used: sub_eq_add_neg, CategoryTheory.ShortComplex.opcyclesMap'_add, CategoryTheory.ShortComplex.opcyclesMap'_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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap (-φ)) (-rightHomologyMap φ)

Tactic:
rightHomologyMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_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₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ Eq (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap (-φ)) (-opcyclesMap φ)

Tactic:
opcyclesMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap'_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₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ rightHomologyMap (φ + φ') =
    HAdd.hAdd (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ) (rightHomologyMap φ')

Tactic:
rightHomologyMap'_add _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_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₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ opcyclesMap (φ + φ') = HAdd.hAdd (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (opcyclesMap φ')

Tactic:
opcyclesMap'_add _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap'_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₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ rightHomologyMap (φ - φ') =
    HSub.hSub (α := S₁.rightHomology ⟶ S₂.rightHomology) (rightHomologyMap φ) (rightHomologyMap φ')

Tactic:
rightHomologyMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.rightHomology, CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.rightHomologyMap'_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₂ : ShortComplex.{v_1, u_1} C
φ φ' : S₁ ⟶ S₂
inst_2 : S₁.HasRightHomology
inst_3 : S₂.HasRightHomology
⊢ opcyclesMap (φ - φ') = HSub.hSub (α := S₁.opcycles ⟶ S₂.opcycles) (opcyclesMap φ) (opcyclesMap φ')

Tactic:
opcyclesMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.opcyclesMap'_sub, CategoryTheory.ShortComplex.opcyclesMap
-- 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₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' (-φ) h₁ h₂ = -homologyMap' φ h₁ h₂

Tactic:
leftHomologyMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_neg, CategoryTheory.ShortComplex.homologyMap'
-- 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₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' (φ + φ') h₁ h₂ = homologyMap' φ h₁ h₂ + homologyMap' φ' h₁ h₂

Tactic:
leftHomologyMap'_add _ _

Premises used: CategoryTheory.ShortComplex.homologyMap', 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₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ homologyMap' (φ - φ') h₁ h₂ = homologyMap' φ h₁ h₂ - homologyMap' φ' h₁ h₂

Tactic:
leftHomologyMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_sub, CategoryTheory.ShortComplex.homologyMap'
-- 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₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ Eq (α := S₁.homology ⟶ S₂.homology) (homologyMap (-φ)) (-homologyMap φ)

Tactic:
homologyMap'_neg _ _

Premises used: CategoryTheory.ShortComplex.homologyMap'_neg, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- 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₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ homologyMap (φ + φ') = HAdd.hAdd (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (homologyMap φ')

Tactic:
homologyMap'_add _ _

Premises used: CategoryTheory.ShortComplex.homologyMap'_add, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- 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₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
⊢ homologyMap (φ - φ') = HSub.hSub (α := S₁.homology ⟶ S₂.homology) (homologyMap φ) (homologyMap φ')

Tactic:
homologyMap'_sub _ _

Premises used: CategoryTheory.ShortComplex.homologyMap'_sub, CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap
-- 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₀ + (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁)
⊢ φ₂.τ₁ = S₁.f ≫ (-h.h₁) + -h.h₀ + φ₁.τ₁

Tactic:
rw [h.comm₁, comp_neg]

Premises used: CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.Preadditive.comp_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 φ₁ φ₂
⊢ φ₂.τ₁ = -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 [h.comm₂, comp_neg, neg_comp]

Premises used: CategoryTheory.Preadditive.comp_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 [h.comm₃, neg_comp]

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

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

Premises used: neg_add_rev, CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.Preadditive.comp_neg, CategoryTheory.ShortComplex.neg_τ₁