awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ p + n = q + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
p q : ℤ
hpq : p + m = q
⊢ (Cochain.comp (G := mappingCocone φ) (liftCochain φ α β h) (snd φ) ⋯).v p q hpq = β.v p q hpq

Tactic:
simp [Cochain.comp_v (n₁ := n) (n₂ := -1) (n₁₂ := m) _ _ _ p _ _ (by lia)
    (Int.add_neg_cancel_right q 1)]

Premises used: CochainComplex.HomComplex.Cochain.comp_v, Int.add_neg_cancel_right, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
dsimp :
  δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n ⋯) =
    HSub.hSub (α := Cochain M (mappingCocone φ) n')
      ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) ⋯)
      ((δ m n β + α.comp (Cochain.ofHom φ) ⋯).comp
        (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')
⊢ δ n n' (liftCochain φ α β h) =
    HSub.hSub (α := Cochain M (mappingCocone φ) n') ((δ n n' α).comp (inl φ) ⋯)
      ((δ m n β + α.comp (Cochain.ofHom φ) ⋯).comp (↑(inr φ) : Cochain L (mappingCocone φ) 1) hn')

Tactic:
dsimp [liftCochain, inl, inr]

Premises used: CochainComplex.mappingCocone.inr, CochainComplex.mappingCocone.inl, CochainComplex.mappingCocone.liftCochain
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
h₁ :
  ∀ (p q : ℤ) (hpq : p + n' = q),
    Cochain.v (δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n ⋯)) p q hpq =
      (HSub.hSub (α := Cochain M (mappingCocone φ) n')
            ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) ⋯)
            ((δ m n β + α.comp (Cochain.ofHom φ) ⋯).comp
              (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')).v
        p q hpq
⊢ δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n ⋯) =
    HSub.hSub (α := Cochain M (mappingCocone φ) n')
      ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) ⋯)
      ((δ m n β + α.comp (Cochain.ofHom φ) ⋯).comp
        (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ n' + -1 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ p + n = q + -1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ q + -1 + 1 = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
h₁ :
  HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q)
      ((δ n n' α).v p q hpq ≫ Cochain.v (mappingCone.inl φ) q (q + -1) ⋯ : M.X p ⟶ (mappingCone φ).X (q + -1))
      (HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q) (β := M.X p ⟶ (mappingCocone φ).X q)
        (-(δ m n β).v p (q + -1) ⋯ ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
        (-α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)) =
    HSub.hSub (α := M.X p ⟶ (mappingCocone φ).X q)
      ((δ n n' α).v p q hpq ≫ Cochain.v (mappingCone.inl φ) q (q + -1) ⋯ : M.X p ⟶ (mappingCocone φ).X q)
      (HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q) (β := M.X p ⟶ (mappingCocone φ).X q)
        ((δ m n β).v p (q + -1) ⋯ ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
        (α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q))
⊢ Cochain.v (δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n ⋯)) p q hpq =
    (HSub.hSub (α := Cochain M (mappingCocone φ) n')
          ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) ⋯)
          ((δ m n β + α.comp (Cochain.ofHom φ) ⋯).comp
            (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')).v
      p q hpq

Tactic:
simp [mappingCone.δ_liftCochain _ _ _ _ n' hn',
    Cochain.δ_rightShift _ (-1) _ n' _ n (by lia),
    Cochain.rightShift_v (n := n) _ _ _ _ p _ _ (q + -1) (by lia),
    Cochain.rightShift_v _ _ _ _ _ _ _ (q + -1) rfl,
    Cochain.rightShift_v _ _ _ _ _ _ _ _ (add_zero (q + -1)),
    Cochain.comp_v _ _ _ p q _ hpq rfl,
    Cochain.comp_v (n₁ := n) (n₂ := 1) _ _ _ p (q + -1) q (by lia) (by lia)]

Premises used: CochainComplex.HomComplex.Cochain.comp_v, HAdd.hAdd, CochainComplex.mappingCone.δ_liftCochain, CochainComplex.HomComplex.Cochain.δ_rightShift, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cochain M K n
β : Cochain M L m
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n' = q
⊢ HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q)
      ((δ n n' α).v p q hpq ≫ Cochain.v (mappingCone.inl φ) q (q + -1) ⋯ : M.X p ⟶ (mappingCone φ).X (q + -1))
      (HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q) (β := M.X p ⟶ (mappingCocone φ).X q)
        (-(δ m n β).v p (q + -1) ⋯ ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
        (-α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)) =
    HSub.hSub (α := M.X p ⟶ (mappingCocone φ).X q)
      ((δ n n' α).v p q hpq ≫ Cochain.v (mappingCone.inl φ) q (q + -1) ⋯ : M.X p ⟶ (mappingCocone φ).X q)
      (HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q) (β := M.X p ⟶ (mappingCocone φ).X q)
        ((δ m n β).v p (q + -1) ⋯ ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
        (α.v p (q + -1) ⋯ ≫ φ.f (q + -1) ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q))

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
n m : ℤ
α : Cocycle M K n
β : Cochain M L m
h : m + 1 = n
hαβ : δ m n β + (↑α : Cochain M K n).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Membership.mem (γ := AddSubgroup (Cochain M (mappingCocone φ) n)) (cocycle M (mappingCocone φ) n)
    (liftCochain φ (↑α : Cochain M K n) β h)

Tactic:
simp [Cocycle.mem_iff _ _ rfl, δ_liftCochain _ _ _ _ _ rfl, hαβ]

Premises used: CochainComplex.mappingCocone.δ_liftCochain, rfl, CochainComplex.HomComplex.Cocycle.mem_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ δ (-1) 0 β + (↑(Cocycle.ofHom α) : Cochain M K 0).comp (Cochain.ofHom φ) ⋯ = 0

Tactic:
simpa [← Cochain.ofHom_comp]

Premises used: CochainComplex.HomComplex.Cochain.ofHom_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ Eq (α := Cochain M (mappingCocone φ) 0) (Cochain.ofHom (lift φ α β hαβ))
    (liftCochain φ (Cochain.ofHom α) β lift._proof_1)

Tactic:
simp [lift]

Premises used: CochainComplex.mappingCocone.lift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
p : ℤ
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Hom.f (lift φ α β hαβ) p) (Hom.f (fst φ) p) = α.f p

Tactic:
simp [lift]

Premises used: CochainComplex.mappingCocone.lift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasHomotopyCofiber φ
M : CochainComplex.{v_1, u_1, 0} C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
p q : ℤ
hpq : p + -1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Hom.f (lift φ α β hαβ) p) (Cochain.v (snd φ) p q hpq) = β.v p q hpq

Tactic:
simp [lift]

Premises used: CochainComplex.mappingCocone.lift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ HAdd.hAdd (α := ℤ) (-1) 1 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ (triangle φ).rotate.mor₁ ≫ Iso.hom (Iso.refl (triangle φ).rotate.obj₂) =
    Iso.hom (Iso.refl (triangle φ).rotate.obj₁) ≫ (mappingCone.triangle φ).mor₁

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
⊢ (triangle φ).rotate.mor₂ ≫
      Iso.hom
        (Iso.app (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2) (mappingCone φ)) =
    Iso.hom (Iso.refl (triangle φ).rotate.obj₂) ≫ (mappingCone.triangle φ).mor₂

Tactic:
simp [triangle]

Premises used: CochainComplex.mappingCocone.triangle
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
refine :
  (triangle φ).rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangle φ).rotate.obj₁)) =
    Iso.hom
        (Iso.app (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2) (mappingCone φ)) ≫
      (mappingCone.triangle φ).mor₃
⊢ (triangle φ).rotate ≅ mappingCone.triangle φ

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
    ((shiftFunctorCompIsoId _ (-1 : ℤ) 1 (by lia)).app _)
    (by simp) (by simp [triangle]) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Pretriangulated.Triangle.isoMk
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
dsimp :
  (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (fst φ)) ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K) =
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
        (mappingCone φ) ≫
      (mappingCone.triangle φ).mor₃
⊢ (triangle φ).rotate.mor₃ ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
        (Iso.hom (Iso.refl (triangle φ).rotate.obj₁)) =
    Iso.hom
        (Iso.app (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2) (mappingCone φ)) ≫
      (mappingCone.triangle φ).mor₃

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
h :
  ∀ (n : ℤ),
    Hom.f
        ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
              (fst φ)) ≫
          CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K))
        n =
      Hom.f
        (NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
            (mappingCone φ) ≫
          (mappingCone.triangle φ).mor₃)
        n
⊢ (-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (fst φ)) ≫
      CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K) =
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
        (mappingCone φ) ≫
      (mappingCone.triangle φ).mor₃

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℤ
φ : K ⟶ L
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
n : ℤ
⊢ Hom.f
      ((-CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1)
            (fst φ)) ≫
        CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) 1) (𝟙 K))
      n =
    Hom.f
      (NatTrans.app (Iso.hom (shiftFunctorCompIsoId (CochainComplex.{v_1, u_1, 0} C ℤ) (-1) 1 triangle._proof_2))
          (mappingCone φ) ≫
        (mappingCone.triangle φ).mor₃)
      n

Tactic:
simp [fst, mappingCone.triangle, Cochain.leftShift_v _ _ _ _ _ _ _ _ rfl,
    Cochain.rightShift_v _ _ _ _ _ _ _ _ rfl,
    shiftFunctorCompIsoId, shiftFunctorAdd'_inv_app_f', shiftFunctorZero_hom_app_f]

Premises used: CochainComplex.shiftFunctorAdd'_inv_app_f', CochainComplex.mappingCocone.fst, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.shiftFunctorCompIsoId, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.mappingCone.triangle, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
ι : Type u_3
inst_4 : AddRightCancelSemigroup ι
inst_5 : One ι
F G : CochainComplex.{v, u_1, u_3} C ι
φ : F ⟶ G
inst_6 : ∀ (p : ι), HasBinaryBiproduct.{v, u_1} (F.X (p + 1)) (G.X p)
i : ι
⊢ HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i : ℤ
⊢ HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)

Tactic:
have := HasHomotopyCofiber.hasBinaryBiproduct φ i (i + 1) rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i : ℤ
this : HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)
rw : IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (biprod.{v, u_1} (F.X (i + 1)) (G.X i))
⊢ IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (F.X (i + 1)) ∧ IsZero.{v, u_1} (G.X i)

Tactic:
rw [← biprod_isZero_iff]

Premises used: CategoryTheory.Limits.biprod_isZero_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i : ℤ
this : HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)
⊢ IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (biprod.{v, u_1} (F.X (i + 1)) (G.X i))

Tactic:
(homotopyCofiber.XIsoBiprod φ i (i + 1) rfl).isZero_iff

Premises used: HomologicalComplex.homotopyCofiber.X, dite, CategoryTheory.Iso.isZero_iff, HAdd.hAdd, HomologicalComplex.homotopyCofiber.XIsoBiprod, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
i : ℤ
this : HasBinaryBiproduct.{v, u_1} (F.X (i + 1)) (G.X i)
⊢ IsZero.{v, u_1} ((mappingCone φ).X i) ↔ IsZero.{v, u_1} (biprod.{v, u_1} (F.X (i + 1)) (G.X i))

Tactic:
exact (homotopyCofiber.XIsoBiprod φ i (i + 1) rfl).isZero_iff

Premises used: CategoryTheory.Iso.isZero_iff, HAdd.hAdd, HomologicalComplex.homotopyCofiber.XIsoBiprod, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p q : ℤ
hpq : p + -1 = q
⊢ q + 1 = p

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
h :
  ∀ (p : ℤ),
    Eq.{v + 1} (α := (mappingCone φ).X p ⟶ F.X (p + 2))
      (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (hpq : p + 1 = q) ↦ homotopyCofiber.fstX φ p q hpq)) p (p + 2) ⋯)
      (Cochain.v 0 p (p + 2) ⋯)
⊢ Eq.{v + 1} (α := Cochain (mappingCone φ) F 2)
    (δ 1 2 (Cochain.mk fun (p q : ℤ) (hpq : p + 1 = q) ↦ homotopyCofiber.fstX φ p q hpq)) 0

Tactic:
ext p _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p : ℤ
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p : ℤ
⊢ p + 2 = p + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p : ℤ
⊢ p + 1 = p + 2 - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p : ℤ
⊢ Int.negOnePow 2 = 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p : ℤ
⊢ Eq.{v + 1} (α := (mappingCone φ).X p ⟶ F.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (hpq : p + 1 = q) ↦ homotopyCofiber.fstX φ p q hpq)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)

Tactic:
simp [δ_v 1 2 (by lia) _ p (p + 2) (by lia) (p + 1) (p + 1) (by lia) rfl,
      homotopyCofiber.d_fstX φ p (p + 1) (p + 2) rfl, mappingCone,
      show Int.negOnePow 2 = 1 by rfl]

Premises used: CochainComplex.HomComplex.δ_v, CochainComplex.mappingCone, HomologicalComplex.homotopyCofiber.d_fstX, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : Category.{v', u_2} D
inst_2 : Preadditive.{v, u_1} C
inst_3 : Preadditive.{v', u_2} D
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_4 : HasHomotopyCofiber φ
p q : ℤ
hpq : q + 1 = p
rw : q + 1 + -1 = q
rw₁ rw₂ : q = q
⊢ p + -1 = q

Tactic:
rw [← hpq, add_neg_cancel_right]

Premises used: add_neg_cancel_right
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
F G : CochainComplex.{v, u_1, 0} C ℤ
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
p q : ℤ
hpq : q + 1 = p
⊢ CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q ⋯)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) q p hpq) =
    𝟙 (F.X p)

Tactic:
simp [inl, fst]

Premises used: CochainComplex.mappingCone.fst, CochainComplex.mappingCone.inl