awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.Plus.{v_1, u_1} C
f₀ f₁ : K.obj (P := CochainComplex.plus C) ⟶ L.obj (P := CochainComplex.plus C)
hf : Homotopy f₀ f₁
⊢ ∃ (P : Precylinder K) (x :
    P.LeftHomotopy (ObjectProperty.homMk (P := CochainComplex.plus C) f₀)
      (ObjectProperty.homMk (P := CochainComplex.plus C) f₁)),
    MorphismProperty.inverseImage (homotopyEquivalences C (ComplexShape.up ℤ)) (CochainComplex.Plus.ι C) P.π

Tactic:
exact ⟨K.precylinder, Precylinder.LeftHomotopy.fullSubcategoryEquiv.symm
      { h := cylinder.desc _ _ hf }, ⟨cylinder.homotopyEquiv _ (fun n ↦ ⟨n - 1, by simp⟩), rfl⟩⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
X : C
rw : CochainComplex.plus.{v_1, u_1} C (Functor.obj (CochainComplex.singleFunctor C n) X)
⊢ plus.{v_1, u_1} C (Functor.obj (singleFunctor C n) X)

Tactic:
rw [← quotient_obj_singleFunctors_obj, plus_quotient_obj_iff]

Premises used: HomotopyCategory.plus_quotient_obj_iff, HomotopyCategory.quotient_obj_singleFunctors_obj
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
X : C
⊢ CochainComplex.plus.{v_1, u_1} C (Functor.obj (CochainComplex.singleFunctor C n) X)

Tactic:
⟨n, inferInstance⟩

Premises used: inferInstance, Exists.intro, CochainComplex.plus
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
X : C
⊢ CochainComplex.plus.{v_1, u_1} C (Functor.obj (CochainComplex.singleFunctor C n) X)

Tactic:
exact ⟨n, inferInstance⟩
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
A : Type u_2
inst_2 : Category.{v_2, u_2} A
inst_3 : Abelian.{v_2, u_2} A
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
⊢ Functor.Additive (D := Plus.{v_1, u_1} C) (ObjectProperty.lift (plus C) (HomotopyCategory.singleFunctor C n) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
rw : p = p + -1 + 1
rw₁ rw₂ : p = p
⊢ p = q + 1

Tactic:
rw [← hpq, neg_add_cancel_right]

Premises used: neg_add_cancel_right
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
dsimp :
  CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q hpq)
      (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) q q ⋯) =
    -(HomologicalComplex.XIsoOfEq K ⋯).inv
⊢ Cochain.v (inl φ) p q hpq ≫ (triangle φ).mor₃.f q = -(K.shiftFunctorObjXIso 1 q p ⋯).inv

Tactic:
dsimp [triangle]

Premises used: CochainComplex.mappingCone.triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ q + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p q : ℤ
hpq : p + -1 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q hpq)
      (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) q q ⋯) =
    -(HomologicalComplex.XIsoOfEq K ⋯).inv

Tactic:
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
    Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by lia), shiftFunctor_obj_X,
    shiftFunctorObjXIso, Preadditive.comp_neg, inl_v_fst_v_assoc]

Premises used: CochainComplex.HomComplex.Cochain.neg_v, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CochainComplex.shiftFunctor_obj_X, CochainComplex.shiftFunctorObjXIso, zero_add, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.rightShift_neg, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.mappingCone.inl_v_fst_v_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
dsimp :
  CategoryStruct.comp (Y := (mappingCone φ).X p) (HomologicalComplex.Hom.f (inr φ) p)
      (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) p p ⋯) =
    0
⊢ HomologicalComplex.Hom.f (inr φ) p ≫ (triangle φ).mor₃.f p = 0

Tactic:
dsimp [triangle]

Premises used: CochainComplex.mappingCone.triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
p : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (HomologicalComplex.Hom.f (inr φ) p)
      (Cochain.v (Cochain.rightShift (-(↑(fst φ) : Cochain (mappingCone φ) K 1)) 1 0 triangle._proof_3) p p ⋯) =
    0

Tactic:
simp only [Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
    Cochain.rightShift_v _ 1 0 _ p p (add_zero p) (p + 1) rfl, shiftFunctor_obj_X,
    shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id,
    Preadditive.comp_neg, inr_f_fst_v, neg_zero]

Premises used: CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.HomComplex.Cochain.neg_v, HomologicalComplex.XIsoOfEq_rfl, CategoryTheory.Preadditive.comp_neg, CochainComplex.shiftFunctor_obj_X, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_inv, HAdd.hAdd, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.rightShift_neg, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, neg_zero, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
h : ∀ (i : ℤ), (inr φ ≫ (triangle φ).mor₃).f i = HomologicalComplex.Hom.f 0 i
⊢ inr φ ≫ (triangle φ).mor₃ = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
i : ℤ
⊢ (inr φ ≫ (triangle φ).mor₃).f i = HomologicalComplex.Hom.f 0 i

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ Cochain.comp (inl (𝟙 K)) (Cochain.ofHom (𝟙 (mappingCone (𝟙 K)))) ⋯ =
    HAdd.hAdd (α := Cochain K (mappingCone (𝟙 K)) (-1)) (δ (-2) (-1) 0) ((Cochain.ofHom (𝟙 K)).comp (inl (𝟙 K)) ⋯) +
      Cochain.comp (G := mappingCone (𝟙 K)) (inl (𝟙 K)) (Cochain.ofHom 0) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
⊢ Cochain.ofHom (inr (𝟙 K) ≫ 𝟙 (mappingCone (𝟙 K))) =
    HAdd.hAdd (α := Cochain K (mappingCone (𝟙 K)) 0) (δ (-1) 0 (inl (𝟙 K)))
      (Cochain.ofHom (CategoryStruct.comp (Y := mappingCone (𝟙 K)) (inr (𝟙 K)) 0))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ δ (-1) 0
      (HAdd.hAdd (α := Cochain K₁ (mappingCone φ₂) (-1)) ((Cochain.ofHom a).comp (inl φ₂) ⋯)
        (Cochain.comp
          (↑((Cochain.equivHomotopy (φ₁ ≫ b) (a ≫ φ₂) :
                  (a_1 : Homotopy (φ₁ ≫ b) (a ≫ φ₂)) →
                    { z : Cochain K₁ L₂ (-1) // Cochain.ofHom (φ₁ ≫ b) = δ (-1) 0 z + Cochain.ofHom (a ≫ φ₂) })
                H) :
            Cochain K₁ L₂ (-1))
          (Cochain.ofHom (inr φ₂)) ⋯)) =
    Cochain.ofHom (φ₁ ≫ b ≫ inr φ₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α := L₁ ⟶ mappingCone φ₂)
    (CategoryStruct.comp (Y := mappingCone φ₁) (inr φ₁ : L₁ ⟶ mappingCone φ₁)
        (mapOfHomotopy H : mappingCone φ₁ ⟶ mappingCone φ₂) :
      L₁ ⟶ mappingCone φ₂)
    (b ≫ inr φ₂ : L₁ ⟶ mappingCone φ₂)

Tactic:
simp [mapOfHomotopy]

Premises used: CochainComplex.mappingCone.mapOfHomotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
h :
  ∀ (p : ℤ),
    HomologicalComplex.Hom.f (mapOfHomotopy H ≫ (triangle φ₂).mor₃) p =
      ((triangle φ₁).mor₃ ≫
            CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a).f
        p
⊢ mapOfHomotopy H ≫ (triangle φ₂).mor₃ =
    (triangle φ₁).mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a

Tactic:
ext p
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
h :
  Eq (α := (mappingCone φ₁).X p ⟶ K₂.X (p + 1))
    (HomologicalComplex.Hom.f
        (desc φ₁
          (HAdd.hAdd (α := Cochain K₁ (mappingCone φ₂) (-1)) ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy._proof_2)
            ((Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy._proof_3))
          (b ≫ inr φ₂) ⋯)
        p ≫
      Cochain.v (Cochain.rightShift (-(↑(fst φ₂) : Cochain (mappingCone φ₂) K₂ 1)) 1 0 triangle._proof_3) p p ⋯)
    (Cochain.v (Cochain.rightShift (-(↑(fst φ₁) : Cochain (mappingCone φ₁) K₁ 1)) 1 0 triangle._proof_3) p p ⋯ ≫
      a.f (p + 1))
⊢ HomologicalComplex.Hom.f (mapOfHomotopy H ≫ (triangle φ₂).mor₃) p =
    ((triangle φ₁).mor₃ ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) a).f
      p

Tactic:
dsimp [mapOfHomotopy, triangle]

Premises used: CochainComplex.mappingCone.mapOfHomotopy, CochainComplex.mappingCone.triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
K₁ L₁ K₂ L₂ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ Eq (α := (mappingCone φ₁).X p ⟶ K₂.X (p + 1))
    (HomologicalComplex.Hom.f
        (desc φ₁
          (HAdd.hAdd (α := Cochain K₁ (mappingCone φ₂) (-1)) ((Cochain.ofHom a).comp (inl φ₂) mapOfHomotopy._proof_2)
            ((Cochain.ofHomotopy H).comp (Cochain.ofHom (inr φ₂)) mapOfHomotopy._proof_3))
          (b ≫ inr φ₂) ⋯)
        p ≫
      Cochain.v (Cochain.rightShift (-(↑(fst φ₂) : Cochain (mappingCone φ₂) K₂ 1)) 1 0 triangle._proof_3) p p ⋯)
    (Cochain.v (Cochain.rightShift (-(↑(fst φ₁) : Cochain (mappingCone φ₁) K₁ 1)) 1 0 triangle._proof_3) p p ⋯ ≫
      a.f (p + 1))

Tactic:
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
    Cochain.rightShift_v _ 1 0 _ p p _ (p + 1) rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Preadditive.comp_neg,
    Preadditive.neg_comp, ext_from_iff _ _ _ rfl, inl_v_desc_f_assoc, Cochain.add_v,
    Cochain.zero_cochain_comp_v, Cochain.ofHom_v, Cochain.comp_zero_cochain_v, Preadditive.add_comp,
    assoc, inl_v_fst_v, inr_f_fst_v, comp_zero, add_zero, inl_v_fst_v_assoc, inr_f_desc_f_assoc,
    HomologicalComplex.comp_f, neg_zero, inr_f_fst_v_assoc, zero_comp, and_self]

Premises used: CategoryTheory.Category.assoc, CochainComplex.mappingCone.inr_f_fst_v, and_self, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.HomComplex.Cochain.neg_v, HomologicalComplex.XIsoOfEq_rfl, Int.reduceNeg, CategoryTheory.Preadditive.comp_neg, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CategoryTheory.Limits.comp_zero, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingCone.ext_from_iff, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.mappingCone.inl_v_desc_f_assoc, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Category.comp_id, HomologicalComplex.comp_f, CochainComplex.mappingCone.inl_v_fst_v, CategoryTheory.Preadditive.add_comp, CategoryTheory.Iso.refl_inv, CochainComplex.mappingCone.inr_f_fst_v_assoc, HAdd.hAdd, CochainComplex.shiftFunctor_obj_X', CategoryTheory.Preadditive.neg_comp, CategoryTheory.Limits.zero_comp, CochainComplex.HomComplex.Cochain.rightShift_neg, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, neg_zero, CochainComplex.HomComplex.Cochain.add_v, CochainComplex.mappingCone.inl_v_fst_v_assoc, rfl, CochainComplex.mappingCone.inr_f_desc_f_assoc
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
dsimp :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₁ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₂)
⊢ Eq (α := (triangleh φ₁).obj₁ ⟶ (triangleh φ₂).obj₂)
    ((triangleh φ₁).mor₁ ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫ (triangleh φ₂).mor₁)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
simp :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (φ₁ ≫ b))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (a ≫ φ₂))
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₁ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) a ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) φ₂)

Tactic:
simp only [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (φ₁ ≫ b))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (a ≫ φ₂))

Tactic:
HomotopyCategory.eq_of_homotopy _ _ H

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₂)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (φ₁ ≫ b))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (a ≫ φ₂))

Tactic:
exact HomotopyCategory.eq_of_homotopy _ _ H

Premises used: HomotopyCategory.eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
dsimp :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₁) :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂)) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b ≫
        CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₂) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
⊢ Eq (α := (triangleh φ₁).obj₂ ⟶ (triangleh φ₂).obj₃)
    ((triangleh φ₁).mor₂ ≫
      CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b ≫ (triangleh φ₂).mor₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasBinaryBiproducts.{v_1, u_1} C
inst_4 : Preadditive.{v_2, u_2} D
inst_5 : HasBinaryBiproducts.{v_2, u_2} D
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex.{v_1, u_1, 0} C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryStruct.comp (Y := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₁) :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁))
        (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mapOfHomotopy H) :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₁) ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂)) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) b ≫
        CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (inr φ₂) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L₁ ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) (mappingCone φ₂))

Tactic:
simp only [← Functor.map_comp, triangleMapOfHomotopy_comm₂]

Premises used: CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, CategoryTheory.Functor.map_comp