awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₁) ⋯ =
    δ (-1) 0 γ₂ + Cochain.comp (Cochain.ofHom (inr φ)) (Cochain.ofHom f₂) ⋯
⊢ Cochain.ofHom f₁ = δ (-1) 0 (descCochain φ γ₁ γ₂ descHomotopy._proof_1) + Cochain.ofHom f₂

Tactic:
simp [ext_cochain_from_iff _ _ _ (neg_add_cancel 1),
      δ_descCochain _ _ _ _ _ (neg_add_cancel 1), h₁, h₂]

Premises used: CochainComplex.mappingCone.ext_cochain_from_iff, neg_add_cancel, CochainComplex.mappingCone.δ_descCochain, OfNat.ofNat
-- 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 K F m
β : Cochain K G n
h : n + 1 = m
⊢ 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 K F m
β : Cochain K G n
h : n + 1 = m
⊢ Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (↑(fst φ) : Cochain (mappingCone φ) F 1) h = α

Tactic:
simp [liftCochain]

Premises used: CochainComplex.mappingCone.liftCochain
-- 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 K F m
β : Cochain K G n
h : n + 1 = m
⊢ Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (snd φ) ⋯ = β

Tactic:
simp [liftCochain]

Premises used: CochainComplex.mappingCone.liftCochain
-- 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 K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = 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 K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = 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 K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) p₂ p₃ h₂₃) =
    α.v p₁ p₃ ⋯

Tactic:
simpa only [Cochain.comp_v _ _ h p₁ p₂ p₃ h₁₂ h₂₃]
    using Cochain.congr_v (liftCochain_fst φ α β h) p₁ p₃ (by lia)

Premises used: CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.mappingCone.liftCochain_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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
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 K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (snd φ) p₂ p₂ ⋯) =
    β.v p₁ p₂ h₁₂

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

Premises used: CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.congr_v, CochainComplex.mappingCone.liftCochain_snd, add_zero
-- 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 K F m
β : Cochain K G n
h : n + 1 = m
m' : ℤ
hm' : m + 1 = m'
⊢ m' + -1 = 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 K F m
β : Cochain K G n
h : n + 1 = m
m' : ℤ
hm' : m + 1 = m'
simp :
  HAdd.hAdd (α := Cochain K (mappingCone φ) m) (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯)
        (-(δ m m' α).comp (inl φ) ⋯) +
      (δ n m β).comp (Cochain.ofHom (inr φ)) ⋯ =
    -(δ m m' α).comp (inl φ) ⋯ +
      HAdd.hAdd (α := Cochain K (mappingCone φ) m) ((δ n m β).comp (Cochain.ofHom (inr φ)) ⋯)
        (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯)
⊢ δ n m (HAdd.hAdd (α := Cochain K (mappingCone φ) n) (α.comp (inl φ) ⋯) (β.comp (Cochain.ofHom (inr φ)) ⋯)) =
    HAdd.hAdd (α := Cochain K (mappingCone φ) m) (-(δ m m' α).comp (inl φ) ⋯)
      ((δ n m β + α.comp (Cochain.ofHom φ) ⋯).comp (Cochain.ofHom (inr φ)) ⋯)

Tactic:
simp only [δ_add, δ_comp α (inl φ) _ m' _ _ h hm' (neg_add_cancel 1),
    δ_comp_zero_cochain _ _ _ h, δ_inl, Cochain.ofHom_comp,
    Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
    δ_ofHom, Cochain.comp_zero, zero_add, Cochain.add_comp,
    Cochain.comp_assoc_of_second_is_zero_cochain]

Premises used: CochainComplex.mappingCone.δ_inl, CochainComplex.HomComplex.Cochain.add_comp, CochainComplex.HomComplex.δ_ofHom, Int.negOnePow_neg, Int.negOnePow_one, CochainComplex.HomComplex.δ_comp, zero_add, CochainComplex.HomComplex.δ_add, one_smul, Units.neg_smul, neg_add_cancel, CochainComplex.HomComplex.Cochain.comp_zero, CochainComplex.HomComplex.δ_comp_zero_cochain, OfNat.ofNat, CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain, CochainComplex.mappingCone.inl, CochainComplex.HomComplex.Cochain.ofHom_comp
-- 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 K F m
β : Cochain K G n
h : n + 1 = m
m' : ℤ
hm' : m + 1 = m'
⊢ HAdd.hAdd (α := Cochain K (mappingCone φ) m) (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯)
        (-(δ m m' α).comp (inl φ) ⋯) +
      (δ n m β).comp (Cochain.ofHom (inr φ)) ⋯ =
    -(δ m m' α).comp (inl φ) ⋯ +
      HAdd.hAdd (α := Cochain K (mappingCone φ) m) ((δ n m β).comp (Cochain.ofHom (inr φ)) ⋯)
        (α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯)

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 : ℤ
α : Cocycle K F m
β : Cochain K G n
h : n + 1 = m
eq : δ n m β + (↑α : Cochain K F m).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Eq (α := Cochain K (mappingCone φ) m) (δ n m (liftCochain φ (↑α : Cochain K F m) β h)) 0

Tactic:
simp only [δ_liftCochain φ α β h (m + 1) rfl, eq,
      Cocycle.δ_eq_zero, Cochain.zero_comp, neg_zero, add_zero]

Premises used: CochainComplex.HomComplex.Cocycle.δ_eq_zero, HAdd.hAdd, CochainComplex.mappingCone.δ_liftCochain, CochainComplex.HomComplex.Cochain.zero_comp, add_zero, OfNat.ofNat, neg_zero, 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Eq (α := Cochain K (mappingCone φ) 0) (Cochain.ofHom (lift φ α β eq)) (liftCochain φ (↑α : Cochain K F 1) β ⋯)

Tactic:
simp only [lift, Cocycle.cochain_ofHom_homOf_eq_coe, liftCocycle_coe]

Premises used: CochainComplex.mappingCone.liftCocycle_coe, CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe, CochainComplex.mappingCone.lift
-- 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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (lift φ α β eq) p)
      (Cochain.v (↑(fst φ) : Cochain (mappingCone φ) F 1) p q hpq) =
    (↑α : Cochain K F 1).v p q hpq

Tactic:
simp [lift]

Premises used: CochainComplex.mappingCone.lift
-- 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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (lift φ α β eq)) (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ =
    (↑α : Cochain K F 1)

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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
⊢ q = 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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 0 = q
obtain :
  ∀ (hpq : q + 0 = q),
    CategoryStruct.comp (Y := (mappingCone φ).X q) (Hom.f (lift φ α β eq) q) (Cochain.v (snd φ) q q hpq) = β.v q q hpq
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p) (Hom.f (lift φ α β eq) p) (Cochain.v (snd φ) p q hpq) = β.v p q hpq

Tactic:
obtain rfl : q = p := by lia

Premises used: 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 φ
K : CochainComplex.{v, u_1, 0} C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
q : ℤ
hpq : q + 0 = q
⊢ CategoryStruct.comp (Y := (mappingCone φ).X q) (Hom.f (lift φ α β eq) q) (Cochain.v (snd φ) q q hpq) = β.v q q hpq

Tactic:
simp [lift]

Premises used: CochainComplex.mappingCone.lift
-- 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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
⊢ Cochain.comp (G := mappingCone φ) (Cochain.ofHom (lift φ α β eq)) (snd φ) ⋯ = β

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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega
-- 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 ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ Hom.f (lift φ α β eq) p =
    HAdd.hAdd (α := K.X p ⟶ (mappingCone φ).X p) ((↑α : Cochain K F 1).v p q hpq ≫ Cochain.v (inl φ) q p ⋯)
      (β.v p p ⋯ ≫ Hom.f (inr φ) p)

Tactic:
simp [ext_to_iff _ _ _ hpq]

Premises used: CochainComplex.mappingCone.ext_to_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₂ : K ⟶ mappingCone φ
α : Cochain K F 0
β : Cochain K G (-1)
h₁ :
  (Cochain.ofHom f₁).comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯ =
    -δ 0 1 α + (Cochain.ofHom f₂).comp (↑(fst φ) : Cochain (mappingCone φ) F 1) ⋯
h₂ : (Cochain.ofHom f₁).comp (snd φ) ⋯ = δ (-1) 0 β + α.comp (Cochain.ofHom φ) ⋯ + (Cochain.ofHom f₂).comp (snd φ) ⋯
⊢ Cochain.ofHom f₁ = δ (-1) 0 (liftCochain φ α β ⋯) + Cochain.ofHom f₂

Tactic:
simp [δ_liftCochain _ _ _ _ _ (zero_add 1), ext_cochain_to_iff _ _ _ (zero_add 1), h₁, h₂]

Premises used: CochainComplex.mappingCone.ext_cochain_to_iff, zero_add, CochainComplex.mappingCone.δ_liftCochain, OfNat.ofNat
-- 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ m + m' = 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 φ
K L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
⊢ n + 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
linarith : m + -1 + n' < p → -1 + (n + 1 - m) + -(n + n' - p) + (m + -1 + n' + 1 - p) = 0
linarith₁ : p < m + -1 + n' → -1 + -(n + 1 - m) + (n + n' - p) + (p + 1 - (m + -1 + n')) = 0
⊢ m + -1 + n' = p

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

Tactic:
simp [liftCochain, descCochain,
    Cochain.comp_assoc α (inl φ) _ _ (show -1 + n' = m' by lia) (by linarith)]

Premises used: CochainComplex.HomComplex.Cochain.comp_assoc, CochainComplex.mappingCone.liftCochain, CochainComplex.mappingCone.descCochain, CochainComplex.mappingCone.inl
-- 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
⊢ q + m' = p₃

Tactic:
omega
-- 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
⊢ p₁ + p = 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
⊢ (Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ =
    (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯

Tactic:
have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
eq :
  (Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ =
    (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯
⊢ q + 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 L : CochainComplex.{v, u_1, 0} C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
eq :
  (Cochain.comp (G := mappingCone φ) (liftCochain φ α β h) (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ =
    (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯
⊢ CategoryStruct.comp (Y := (mappingCone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (descCochain φ α' β' h') p₂ p₃ h₂₃) =
    α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃

Tactic:
simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
    Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by lia)] using eq

Premises used: CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.HomComplex.Cochain.add_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 L : CochainComplex.{v, u_1, 0} C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ n' + -1 = n

Tactic:
omega
-- 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 L : CochainComplex.{v, u_1, 0} C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α : Cochain K F 1).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ CategoryStruct.comp (Y := (mappingCone φ).X n) (Hom.f (lift φ α β eq) n) (Hom.f (desc φ α' β' eq') n) =
    (↑α : Cochain K F 1).v n n' hnn' ≫ α'.v n' n ⋯ + β.v n n ⋯ ≫ β'.f n

Tactic:
simp only [lift, desc, Cocycle.homOf_f, liftCocycle_coe, descCocycle_coe, Cocycle.ofHom_coe,
    liftCochain_v_descCochain_v φ α.1 β α' (Cochain.ofHom β') (zero_add 1) (neg_add_cancel 1) 0
    (add_zero 0) n n n (add_zero n) (add_zero n) n' hnn', Cochain.ofHom_v]

Premises used: CochainComplex.mappingCone.liftCocycle_coe, CochainComplex.mappingCone.liftCochain_v_descCochain_v, CochainComplex.HomComplex.Cochain.ofHom_v, zero_add, CochainComplex.mappingCone.descCocycle_coe, CochainComplex.HomComplex.Cocycle.homOf_f, CochainComplex.HomComplex.Cochain.ofHom, neg_add_cancel, CochainComplex.HomComplex.Cocycle.ofHom_coe, CochainComplex.mappingCone.desc, add_zero, OfNat.ofNat, CochainComplex.mappingCone.lift, Subtype.val
-- 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 : CategoryTheory.Functor.{v, v', u_1, u_2} C D
inst_5 : H.Additive
inst_6 :
  HasHomotopyCofiber (F := Functor.obj (H.mapHomologicalComplex (ComplexShape.up ℤ)) F)
    (CategoryTheory.Functor.map (H.mapHomologicalComplex (ComplexShape.up ℤ)) φ)
n m : ℤ
hnm : n + 1 = m
⊢ n + 1 = m

Tactic:
lia