awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 j k : ℤ
hij : i + 1 = j
hjk : j + 1 = k
⊢ (mappingCone φ).d i j ≫ Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) j k hjk =
    -Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ≫ F.d j k

Tactic:
apply homotopyCofiber.d_fstX

Premises used: HomologicalComplex.homotopyCofiber.d_fstX
-- 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 φ
i j : ℤ
hij : i + 1 = j
⊢ i - 1 + 1 = i

Tactic:
lia
-- 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 j : ℤ
hij : i + 1 = j
⊢ i - 1 + 1 = i

Tactic:
lia
-- 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 j : ℤ
hij : i + 1 = j
dsimp :
  homotopyCofiber.d φ i j ≫ Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) j j ⋯ =
    HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (β := homotopyCofiber.X φ i ⟶ G.X j)
      (homotopyCofiber.fstX φ i j hij ≫ φ.f j) (Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) i i ⋯ ≫ G.d i j)
⊢ (mappingCone φ).d i j ≫ Cochain.v (snd φ) j j ⋯ =
    HAdd.hAdd (α := (mappingCone φ).X i ⟶ G.X j) (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) i j hij ≫ φ.f j)
      (Cochain.v (snd φ) i i ⋯ ≫ G.d i j)

Tactic:
dsimp [mappingCone, snd, fst]

Premises used: CochainComplex.mappingCone, CochainComplex.mappingCone.snd, CochainComplex.mappingCone.fst
-- 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 j : ℤ
hij : i + 1 = j
simp :
  homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
    HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (homotopyCofiber.fstX φ i j hij ≫ φ.f j)
      (homotopyCofiber.sndX φ i ≫ G.d i j)
⊢ homotopyCofiber.d φ i j ≫ Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) j j ⋯ =
    HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (β := homotopyCofiber.X φ i ⟶ G.X j)
      (homotopyCofiber.fstX φ i j hij ≫ φ.f j) (Cochain.v (Cochain.ofHoms (homotopyCofiber.sndX φ)) i i ⋯ ≫ G.d i j)

Tactic:
simp only [Cochain.ofHoms_v]

Premises used: CochainComplex.HomComplex.Cochain.ofHoms_v
-- 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 j : ℤ
hij : i + 1 = j
⊢ homotopyCofiber.d φ i j ≫ homotopyCofiber.sndX φ j =
    HAdd.hAdd (α := homotopyCofiber.X φ i ⟶ G.X j) (homotopyCofiber.fstX φ i j hij ≫ φ.f j)
      (homotopyCofiber.sndX φ i ≫ G.d i j)

Tactic:
apply homotopyCofiber.d_sndX

Premises used: HomologicalComplex.homotopyCofiber.d_sndX
-- 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 φ
n : ℤ
⊢ n - 1 + 1 = n

Tactic:
lia
-- 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 φ
n : ℤ
⊢ (mappingCone φ).d (n - 1) n ≫ Cochain.v (snd φ) n n ⋯ =
    HAdd.hAdd (α := (mappingCone φ).X (n - 1) ⟶ G.X n)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) (n - 1) n ⋯ ≫ φ.f n)
      (Cochain.v (snd φ) (n - 1) (n - 1) ⋯ ≫ G.d (n - 1) n)

Tactic:
apply d_snd_v

Premises used: CochainComplex.mappingCone.d_snd_v
-- 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 φ
h :
  ∀ (p : ℤ),
    Eq (α := F.X p ⟶ (mappingCone φ).X p) (Cochain.v (δ (-1) 0 (inl φ)) p p ⋯)
      (Cochain.v (Cochain.ofHom (φ ≫ inr φ)) p p ⋯)
⊢ Eq (α := Cochain F (mappingCone φ) 0) (δ (-1) 0 (inl φ)) (Cochain.ofHom (φ ≫ inr φ))

Tactic:
ext p
-- 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 : ℤ
⊢ p + -1 = p - 1

Tactic:
lia
-- 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 : ℤ
⊢ p + 1 + -1 = p

Tactic:
lia
-- 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 : ℤ
⊢ Eq (α := F.X p ⟶ (mappingCone φ).X p) (Cochain.v (δ (-1) 0 (inl φ)) p p ⋯)
    (Cochain.v (Cochain.ofHom (φ ≫ inr φ)) p p ⋯)

Tactic:
simp [δ_v (-1) 0 (neg_add_cancel 1) (inl φ) p p (add_zero p) _ _ rfl rfl,
    inl_v_d φ p (p - 1) (p + 1) (by lia) (by lia)]

Premises used: CochainComplex.HomComplex.δ_v, HSub.hSub, neg_add_cancel, HAdd.hAdd, CochainComplex.mappingCone.inl_v_d, add_zero, OfNat.ofNat, Neg.neg, rfl, CochainComplex.mappingCone.inl
-- 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 φ
h :
  ∀ (p q : ℤ) (hpq : p + 1 = q),
    Eq (α := (mappingCone φ).X p ⟶ G.X q) (Cochain.v (δ 0 1 (snd φ)) p q hpq)
      (Cochain.v (-Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (Cochain.ofHom φ) ⋯) p q hpq)
⊢ Eq (α := Cochain (mappingCone φ) G 1) (δ 0 1 (snd φ))
    (-Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (Cochain.ofHom φ) ⋯)

Tactic:
ext p q hpq
-- 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 : p + 1 = q
⊢ Eq (α := (mappingCone φ).X p ⟶ G.X q) (Cochain.v (δ 0 1 (snd φ)) p q hpq)
    (Cochain.v (-Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (Cochain.ofHom φ) ⋯) p q hpq)

Tactic:
simp [d_snd_v φ p q hpq]

Premises used: CochainComplex.mappingCone.d_snd_v
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
rw : 1 + m = m + 1
rw₁ rw₂ : m + 1 = m + 1
⊢ 1 + m = n

Tactic:
rw [← h, add_comm]

Premises used: add_comm
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ -1 + n = m

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (descCochain φ α β h) ⋯ = α

Tactic:
simp [descCochain]

Premises used: CochainComplex.mappingCone.descCochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (inr φ)) (descCochain φ α β h) ⋯ = β

Tactic:
simp [descCochain]

Premises used: CochainComplex.mappingCone.descCochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
rw : p₁ + m = p₂ + n
rw₁ : p₁ + m = p₁ + -1 + n
rw₂ : p₁ + m = p₁ + -1 + (m + 1)
rw₃ : p₁ + m = p₁ + -1 + (1 + m)
rw₄ : p₁ + m = p₁ + (-1 + (1 + m))
rw₅ rw₆ : p₁ + m = p₁ + m
⊢ p₁ + m = p₃

Tactic:
rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]

Premises used: add_assoc, add_comm, neg_add_cancel_left
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ -1 + n = m

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + -1 = p₂

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₂ + n = p₃

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ p₁ + m = p₃

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + -1 = p₂
h₂₃ : p₂ + n = p₃
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₂) (Cochain.v (inl φ) p₁ p₂ h₁₂)
      (Cochain.v (descCochain φ α β h) p₂ p₃ h₂₃) =
    α.v p₁ p₃ ⋯

Tactic:
simpa only [Cochain.comp_v _ _ (show -1 + n = m by lia) p₁ p₂ p₃
    (by lia) (by lia)] using
      Cochain.congr_v (inl_descCochain φ α β h) p₁ p₃ (by lia)

Premises used: CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.mappingCone.inl_descCochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₁ + n = p₂

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₁) (Hom.f (inr φ) p₁) (Cochain.v (descCochain φ α β h) p₁ p₂ h₁₂) =
    β.v p₁ p₂ h₁₂

Tactic:
simpa only [Cochain.comp_v _ _ (zero_add n) p₁ p₁ p₂ (add_zero p₁) h₁₂, Cochain.ofHom_v]
    using Cochain.congr_v (inr_descCochain φ α β h) p₁ p₂ (by lia)

Premises used: CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.HomComplex.Cochain.ofHom_v, zero_add, add_zero, CochainComplex.mappingCone.inr_descCochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ 1 + n = n'

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ m + 1 = n

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
simp :
  Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) ⋯ +
      (Cochain.comp (snd φ) (δ n n' β) ⋯ +
        -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
            (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β ⋯) ⋯)) =
    Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) ⋯ +
        -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
            (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β ⋯) ⋯) +
      Cochain.comp (snd φ) (δ n n' β) ⋯
⊢ δ n n'
      (HAdd.hAdd (α := Cochain (mappingCone φ) K n) (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) α ⋯)
        (Cochain.comp (snd φ) β ⋯)) =
    HAdd.hAdd (α := Cochain (mappingCone φ) K n')
      (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
      (Cochain.comp (snd φ) (δ n n' β) ⋯)

Tactic:
simp only [δ_add, Cochain.comp_add, δ_comp (fst φ).1 α _ 2 n n' hn' (by lia) (by lia),
    Cocycle.δ_eq_zero, Cochain.zero_comp, smul_zero, add_zero,
    δ_comp (snd φ) β (zero_add n) 1 n' n' hn' (zero_add 1) hn', δ_snd, Cochain.neg_comp,
    smul_neg, Cochain.comp_assoc_of_second_is_zero_cochain, Cochain.comp_units_smul, ← hn',
    Int.negOnePow_succ, Units.neg_smul, Cochain.comp_neg]

Premises used: CochainComplex.HomComplex.Cochain.comp_neg, CochainComplex.HomComplex.Cochain.comp_add, CochainComplex.HomComplex.Cochain.neg_comp, smul_zero, smul_neg, CochainComplex.HomComplex.δ_comp, zero_add, CochainComplex.HomComplex.δ_add, CochainComplex.HomComplex.Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, Units.neg_smul, CochainComplex.mappingCone.snd, CochainComplex.HomComplex.Cochain.comp_units_smul, CochainComplex.mappingCone.fst, CochainComplex.HomComplex.Cochain.zero_comp, add_zero, OfNat.ofNat, Subtype.val, Int.negOnePow_succ, CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) ⋯ +
      (Cochain.comp (snd φ) (δ n n' β) ⋯ +
        -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
            (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β ⋯) ⋯)) =
    Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) (δ m n α) ⋯ +
        -HSMul.hSMul (β := Cochain (mappingCone φ) K n') n.negOnePow
            (Cochain.comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ((Cochain.ofHom φ).comp β ⋯) ⋯) +
      Cochain.comp (snd φ) (δ n n' β) ⋯

Tactic:
abel
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain F K m
β : Cocycle G K n
h : m + 1 = n
eq : δ m n α = n.negOnePow • (Cochain.ofHom φ).comp (↑β : Cochain G K n) ⋯
⊢ Eq (α := Cochain (mappingCone φ) K (n + 1)) (δ n (n + 1) (descCochain φ α (↑β : Cochain G K n) h)) 0

Tactic:
simp [δ_descCochain _ _ _ _ _ rfl, eq, Int.negOnePow_succ]

Premises used: CochainComplex.mappingCone.δ_descCochain, Int.negOnePow_succ, 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ δ (-1) 0 α = Int.negOnePow 0 • (Cochain.ofHom φ).comp (↑(Cocycle.ofHom β) : Cochain G K 0) ⋯

Tactic:
simp [eq]
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ Eq (α := Cochain (mappingCone φ) K 0) (Cochain.ofHom (desc φ α β eq)) (descCochain φ α (Cochain.ofHom β) ⋯)

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCone.desc
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
h : p + -1 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X q) (Cochain.v (inl φ) p q h) (Hom.f (desc φ α β eq) q) = α.v p q h

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCone.desc
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ Cochain.comp (G := mappingCone φ) (inl φ) (Cochain.ofHom (desc φ α β eq)) ⋯ = α

Tactic:
simp
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (inr φ) p) (Hom.f (desc φ α β eq) p) = β.f p

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCone.desc
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
lia
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
p q : ℤ
hpq : p + 1 = q
⊢ Hom.f (desc φ α β eq) p =
    HAdd.hAdd (α := (mappingCone φ).X p ⟶ K.X p)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) p q hpq ≫ α.v q p ⋯) (Cochain.v (snd φ) p p ⋯ ≫ β.f p)

Tactic:
simp [ext_from_iff _ _ _ hpq]

Premises used: CochainComplex.mappingCone.ext_from_iff
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  Cochain.comp (inl φ) (Cochain.ofHom f₁) ⋯ =
    δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + Cochain.comp (inl φ) (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ HAdd.hAdd (α := ℤ) (-2) 1 = -1

Tactic:
simp
-- 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  Cochain.comp (inl φ) (Cochain.ofHom f₁) ⋯ =
    δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + Cochain.comp (inl φ) (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ Cochain.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₁) ⋯ =
    δ (-1) 0 γ₂ + Cochain.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₂) ⋯

Tactic:
simp only [Cochain.ofHom_comp] at h₂

Premises used: CochainComplex.HomComplex.Cochain.ofHom_comp