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 K M m
β : Cochain L M n
h : m + 1 = n
q r : ℤ
hr : q + m = r
hpq : q + -1 + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) (q + -1) q hpq)
      (Cochain.v (descCochain φ α β h) q r hr) =
    β.v (q + -1) r ⋯

Tactic:
simp [inr, descCochain, mappingCocone, smul_smul,
    Cochain.rightShift_v _ _ _ _ _ _ hpq _ (add_zero (q + -1)),
    Cochain.leftShift_v (n := n) _ _ _ _ _ r _ (q + -1) (by lia)]

Premises used: CochainComplex.mappingCocone.descCochain, CochainComplex.mappingCocone.inr, smul_smul, CochainComplex.mappingCocone, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg
-- 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 K M m
β : Cochain L M n
h : m + 1 = n
⊢ 1 + m = 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 K M m
β : Cochain L M n
h : m + 1 = n
h₁ :
  ∀ (p q : ℤ) (hpq : p + n = q),
    (Cochain.comp (G := mappingCocone φ) (↑(inr φ) : Cochain L (mappingCocone φ) 1) (descCochain φ α β h) ⋯).v p q hpq =
      β.v p q hpq
⊢ Cochain.comp (G := mappingCocone φ) (↑(inr φ) : Cochain L (mappingCocone φ) 1) (descCochain φ α β h) ⋯ = β

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 K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + n = q
⊢ p + 1 + m = 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 K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + n = q
⊢ (Cochain.comp (G := mappingCocone φ) (↑(inr φ) : Cochain L (mappingCocone φ) 1) (descCochain φ α β h) ⋯).v p q hpq =
    β.v p q hpq

Tactic:
simp [Cochain.comp_v (n₂ := m) _ _ _ _ (p + 1) q rfl (by lia)]

Premises used: CochainComplex.HomComplex.Cochain.comp_v, HAdd.hAdd, OfNat.ofNat, 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 K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ -1 + n' = 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 K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
h₁ :
  ∀ (p q : ℤ) (hpq : p + n = q),
    (δ m n
            (HSMul.hSMul (β :=
              Cochain
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                  (mappingCone φ))
                M m)
              (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β h) (-1) m ⋯))).v
        p q hpq =
      (HAdd.hAdd (α :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M n)
            (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
              (δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
            (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ n n' β) ⋯)).v
        p q hpq
⊢ δ m n
      (HSMul.hSMul (β :=
        Cochain
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ)) M
          m)
        (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β h) (-1) m ⋯)) =
    HAdd.hAdd (α :=
      Cochain
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ)) M
        n)
      (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
        (δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
      (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ n n' β) ⋯)

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 K M m
β : Cochain L M n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
p q : ℤ
hpq : p + n = q
h₁ :
  ∀ (β : Cochain L M (m + 1)) (hn' : m + 1 + 1 = n') (hpq : p + (m + 1) = q),
    Cochain.v
        (δ m (m + 1)
          (HSMul.hSMul (β :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M m)
            (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β ⋯) (-1) m ⋯)))
        p q hpq =
      (HAdd.hAdd (α :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M (m + 1))
            (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
              (δ m (m + 1) α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
            (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) n' β) ⋯)).v
        p q hpq
⊢ (δ m n
          (HSMul.hSMul (β :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M m)
            (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β h) (-1) m ⋯))).v
      p q hpq =
    (HAdd.hAdd (α :=
          Cochain
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ))
            M n)
          (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
            (δ m n α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ n n' β) ⋯)).v
      p q hpq

Tactic:
subst h
-- 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 : ℤ
α : Cochain K M m
n' p q : ℤ
β : Cochain L M (m + 1)
hn' : m + 1 + 1 = n'
hpq : p + (m + 1) = q
⊢ n' = m + 2

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 ℤ
m : ℤ
α : Cochain K M m
n' p q : ℤ
β : Cochain L M (m + 1)
hn' : m + 1 + 1 = n'
hpq : p + (m + 1) = q
h :
  ∀ (hn' : m + 1 + 1 = m + 2),
    Cochain.v
        (δ m (m + 1)
          (HSMul.hSMul (β :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M m)
            (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β ⋯) (-1) m ⋯)))
        p q hpq =
      (HAdd.hAdd (α :=
            Cochain
              (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1))
                (mappingCone φ))
              M (m + 1))
            (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
              (δ m (m + 1) α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
            (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) (m + 2) β) ⋯)).v
        p q hpq
⊢ Cochain.v
      (δ m (m + 1)
        (HSMul.hSMul (β :=
          Cochain
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ))
            M m)
          (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β ⋯) (-1) m ⋯)))
      p q hpq =
    (HAdd.hAdd (α :=
          Cochain
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ))
            M (m + 1))
          (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
            (δ m (m + 1) α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) n' β) ⋯)).v
      p q hpq

Tactic:
obtain rfl : n' = m + 2 := by lia

Premises used: 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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ m + 2 + -1 = m + 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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ m + 1 + 1 = m + 2

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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ p + -1 + 1 = p

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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ p + -1 + (m + 2) = 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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
h :
  Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) ⋯ ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) q ⋯ +
      (HSMul.hSMul (β := (mappingCone φ).X (p + -1) ⟶ M.X q) m.negOnePow
          (Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq) +
        Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫
          Cochain.v (δ m (m + 1) α) p q hpq) =
    Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ Cochain.v (δ m (m + 1) α) p q hpq +
        HSMul.hSMul (β := (mappingCone φ).X (p + -1) ⟶ M.X q) m.negOnePow
          (Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq) +
      Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) ⋯ ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) q ⋯
⊢ Cochain.v
      (δ m (m + 1)
        (HSMul.hSMul (β :=
          Cochain
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ))
            M m)
          (-m + 1).negOnePow (Cochain.leftShift (mappingCone.descCochain φ α β ⋯) (-1) m ⋯)))
      p q hpq =
    (HAdd.hAdd (α :=
          Cochain
            (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) (A := ℤ) (-1)) (mappingCone φ))
            M (m + 1))
          (Cochain.comp (Cochain.ofHom (-Cocycle.homOf (Cocycle.leftShift (mappingCone.fst φ) (-1) 0 fst._proof_1)))
            (δ m (m + 1) α + m.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) (m + 2) β) ⋯)).v
      p q hpq

Tactic:
simp [Cochain.δ_leftShift _ (-1) _ (m + 1) _ (m + 2) (by lia),
    mappingCone.δ_descCochain (m := m) (n := m + 1) _ _ _ _ (m + 2) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ p p _ (p + -1) (by lia),
    Cochain.leftShift_v (n := m + 2) _ (-1) _ _ _ q _ (p + -1) (by lia),
    Cochain.leftShift_v _ _ _ _ _ _ _ _ (add_zero (p + -1)),
    Cochain.comp_v (n₁ := 1) _ _ _ (p + -1) p _ (by lia) hpq,
    Cochain.comp_v (n₂ := m + 2) _ _ _ p (p + -1) q rfl (by lia),
    smul_smul, Int.negOnePow_add, Int.negOnePow_even 2 ⟨1, rfl⟩]

Premises used: CochainComplex.HomComplex.Cochain.comp_v, smul_smul, Int.negOnePow_add, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, Exists.intro, Int.negOnePow_even, CochainComplex.mappingCone.δ_descCochain, add_zero, OfNat.ofNat, CochainComplex.HomComplex.Cochain.δ_leftShift, 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 ℤ
m : ℤ
α : Cochain K M m
p q : ℤ
β : Cochain L M (m + 1)
hpq : p + (m + 1) = q
hn' : m + 1 + 1 = m + 2
⊢ Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) ⋯ ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) q ⋯ +
      (HSMul.hSMul (β := (mappingCone φ).X (p + -1) ⟶ M.X q) m.negOnePow
          (Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq) +
        Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫
          Cochain.v (δ m (m + 1) α) p q hpq) =
    Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ Cochain.v (δ m (m + 1) α) p q hpq +
        HSMul.hSMul (β := (mappingCone φ).X (p + -1) ⟶ M.X q) m.negOnePow
          (Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p ⋯ ≫ φ.f p ≫ β.v p q hpq) +
      Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) ⋯ ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) 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 : ℤ
α : Cochain K M m
β : Cocycle L M n
h : m + 1 = n
hαβ : δ m n α + m.negOnePow • (Cochain.ofHom φ).comp (↑β : Cochain L M n) ⋯ = 0
⊢ n + 1 = n + 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 K M m
β : Cocycle L M n
h : m + 1 = n
hαβ : δ m n α + m.negOnePow • (Cochain.ofHom φ).comp (↑β : Cochain L M n) ⋯ = 0
⊢ descCochain φ α (↑β : Cochain L M n) h ∈ cocycle (mappingCocone φ) M m

Tactic:
simp [Cocycle.mem_iff _ n h, δ_descCochain _ _ _ h (n + 1) (by lia), hαβ]

Premises used: HAdd.hAdd, CochainComplex.mappingCocone.δ_descCochain, OfNat.ofNat, 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 ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0
⊢ δ 0 1 α + Int.negOnePow 0 • (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0

Tactic:
simpa
-- 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 ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0
⊢ HAdd.hAdd (α := ℤ) 0 1 = 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 ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0
⊢ Eq (α := Cochain (mappingCocone φ) M 0) (Cochain.ofHom (desc φ α β hαβ))
    (descCochain φ α (↑β : Cochain L M 1) ofHom_desc._proof_2)

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCocone.desc
-- 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 ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0
p : ℤ
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Hom.f (desc φ α β hαβ) p) = α.v p p ⋯

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCocone.desc
-- 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 ℤ
α : Cochain K M 0
β : Cocycle L M 1
hαβ : δ 0 1 α + (Cochain.ofHom φ).comp (↑β : Cochain L M 1) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) p q hpq)
      (Hom.f (desc φ α β hαβ) q) =
    (↑β : Cochain L M 1).v p q hpq

Tactic:
simp [desc]

Premises used: CochainComplex.mappingCocone.desc
-- 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 + -1 = m

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₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₁ + m = p₂ + -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₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ p₂ + -1 + 1 = p₂

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₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂) (Hom.f (fst φ) p₂) =
    α.v p₁ p₂ h₁₂

Tactic:
simp [liftCochain, mappingCocone, fst,
    Cochain.rightShift_v (n := m) _ _ _ _ p₁ _ _ (p₂ + -1) (by lia),
    Cochain.leftShift_v (n := 1) _ _ _ _ _ p₂ _ (p₂ + -1) (by lia)]

Premises used: CochainComplex.mappingCocone.liftCochain, CochainComplex.mappingCocone, CochainComplex.mappingCocone.fst, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, Neg.neg
-- 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₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + -1 = p₃
⊢ p₁ + m = p₃

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₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + -1 = p₃
subst :
  CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (snd φ) p₂ (p₂ + -1) ⋯) =
    β.v p₁ (p₂ + -1) ⋯
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (snd φ) p₂ p₃ h₂₃) =
    β.v p₁ p₃ ⋯

Tactic:
subst h₂₃
-- 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₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (snd φ) p₂ (p₂ + -1) ⋯) =
    β.v p₁ (p₂ + -1) ⋯

Tactic:
simp [liftCochain, mappingCocone, snd,
    Cochain.rightShift_v (n := m) _ _ _ _ p₁ _ _ (p₂ + -1) (by lia),
    Cochain.leftShift_v (n := 0) _ _ _ _ _ _ _ _ (add_zero _),
    Int.negOnePow_even 2 ⟨1, rfl⟩]

Premises used: CochainComplex.mappingCocone.snd, CochainComplex.mappingCocone.liftCochain, CochainComplex.mappingCocone, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, Exists.intro, Int.negOnePow_even, 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
h₁ :
  ∀ (p q : ℤ) (hpq : p + m = q),
    (Cochain.comp (G := mappingCocone φ) (liftCochain φ α β h) (snd φ) ⋯).v p q hpq = β.v p q hpq
⊢ Cochain.comp (G := mappingCocone φ) (liftCochain φ α β h) (snd φ) ⋯ = β

Tactic:
ext p q hpq