awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have hL₁ : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
Tactic: rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have refine_2 : Eq.{max 1 (v_1 + 1)} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
Tactic: rw [hK ((HomotopyCategory.quotient _ _).map f) hL, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK :
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
L : CochainComplex.{v_1, u_1, 0} C ℤ
f : K ⟶ L
hL : HomotopyCategory.subcategoryAcyclic C (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
refine_2 :
  Eq.{max 1 (v_1 + 1)} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    0 (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 0)
have refine_2₁ : Eq.{max 1 (v_1 + 1)} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)
  0 0
Tactic: rw [hK ((HomotopyCategory.quotient _ _).map f) hL, Functor.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
hK : K.IsKProjective
n : ℤ
⊢ (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K).IsKProjective
have rw : ∀
  (hK :
    ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
  (n : ℤ),
  ObjectProperty.leftOrthogonal (HomotopyCategory.subcategoryAcyclic C)
    (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v_1, u_1, 0} C ℤ) n) K))
Tactic: rw [isKProjective_iff_leftOrthogonal] at hK ⊢
Cleared hypotheses: hK, n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
n : ℤ
⊢ Injective.{v_1, u_1} (L.X n)
have dsimp : Injective.{v_1, u_1} (op (K.X (-n)))
Tactic: dsimp [L]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
⊢ K.IsKProjective
have this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
Tactic: have (n : ℤ) : Injective (L.X n) := by
    dsimp [L]
    infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
⊢ L.IsStrictlyGE (-d)
have rw : ∀ (i : ℤ), autoParam (i < -d) isStrictlyGE_iff._auto_1 → IsZero.{v_1, u_1} (L.X i)
Tactic: rw [isStrictlyGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.KProjective (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℤ
d : ℤ
inst_2 : K.IsStrictlyLE d
inst_3 : ∀ (n : ℤ), Projective.{v_1, u_1} (K.X n)
L : CochainComplex.{v_1, u_1, 0} Cᵒᵖ ℤ := Functor.obj (Equivalence.functor (opEquivalence C)) (op K)
this : ∀ (n : ℤ), Injective.{v_1, u_1} (L.X n)
⊢ K.IsKProjective
have this₁ : L.IsStrictlyGE (-d)
Tactic: have : L.IsStrictlyGE (-d) := by
    rw [isStrictlyGE_iff]
    intro i hi
    exact (K.isZero_of_isStrictlyLE d _ (by dsimp; lia)).op
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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 φ
p q : ℤ
hpq : p + -1 = q
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p ⋯) (Cochain.v (snd φ) p q hpq) = 0
have obtain : ∀ (hpq : p + -1 = p + -1),
  CategoryStruct.comp (Y := (mappingCocone φ).X p) (Cochain.v (inl φ) p p sorry) (Cochain.v (snd φ) p (p + -1) hpq) = 0
Tactic: obtain rfl : q = p + -1 := by lia
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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 φ
p q : ℤ
hpq : p + -1 = q
⊢ HAdd.hAdd (α := (mappingCocone φ).X p ⟶ (mappingCocone φ).X p) (Hom.f (fst φ) p ≫ Cochain.v (inl φ) p p ⋯)
      (Cochain.v (snd φ) p q hpq ≫ Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) q p ⋯) =
    𝟙 ((mappingCocone φ).X p)
have obtain : ∀ (hpq : p + -1 = p + -1),
  HAdd.hAdd (α := (mappingCocone φ).X p ⟶ (mappingCocone φ).X p) (Hom.f (fst φ) p ≫ Cochain.v (inl φ) p p sorry)
      (Cochain.v (snd φ) p (p + -1) hpq ≫ Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) (p + -1) p sorry) =
    𝟙 ((mappingCocone φ).X p)
Tactic: obtain rfl : q = p + -1 := by lia
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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 + 1 = q
r : ℤ
hr : q + m = r
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X q) (Cochain.v (↑(inr φ) : Cochain L (mappingCocone φ) 1) p q hpq)
      (Cochain.v (descCochain φ α β h) q r hr) =
    β.v p r ⋯
have obtain : ∀ (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 sorry
Tactic: obtain rfl : p = q + -1 := by lia
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
⊢ Cochain.comp (G := mappingCocone φ) (↑(inr φ) : Cochain L (mappingCocone φ) 1) (descCochain φ α β h) ⋯ = β
have h₁ : ∀ (p q : ℤ) (hpq : p + n = q),
  (Cochain.comp (G := mappingCocone φ) (↑(inr φ) : Cochain L (mappingCocone φ) 1) (descCochain φ α β h) sorry).v p q hpq =
    β.v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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'
⊢ δ 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' β) ⋯)
have 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 sorry))).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 β sorry) sorry)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ n n' β) sorry)).v
      p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
⊢ (δ 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
have 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 φ α β sorry) (-1) m sorry)))
      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 β sorry) sorry)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) n' β) sorry)).v
      p q hpq
Tactic: subst h
Cleared hypotheses: n, β, h, hn', hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
⊢ 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
have 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 φ α β sorry) (-1) m sorry)))
      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 β sorry) sorry)
          (Cochain.comp (Cochain.leftShift (mappingCone.snd φ) (-1) (-1) snd._proof_1) (δ (m + 1) (m + 2) β) sorry)).v
      p q hpq
Tactic: obtain rfl : n' = m + 2 := by lia
Cleared hypotheses: n', hn'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
      (δ 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
have h : Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) sorry ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) q sorry +
    (HSMul.hSMul (β := (mappingCone φ).X (p + -1) ⟶ M.X q) m.negOnePow
        (Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p sorry ≫ φ.f p ≫ β.v p q hpq) +
      Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p sorry ≫ Cochain.v (δ m (m + 1) α) p q hpq) =
  Cochain.v (↑(mappingCone.fst φ) : Cochain (mappingCone φ) K 1) (p + -1) p sorry ≫ 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 sorry ≫ φ.f p ≫ β.v p q hpq) +
    Cochain.v (mappingCone.snd φ) (p + -1) (p + -1) sorry ≫ Cochain.v (δ (m + 1) (m + 2) β) (p + -1) q sorry
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⟩]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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₃
⊢ CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
      (Cochain.v (snd φ) p₂ p₃ h₂₃) =
    β.v p₁ p₃ ⋯
have subst : CategoryStruct.comp (Y := (mappingCocone φ).X p₂) (Cochain.v (liftCochain φ α β h) p₁ p₂ h₁₂)
    (Cochain.v (snd φ) p₂ (p₂ + -1) sorry) =
  β.v p₁ (p₂ + -1) sorry
Tactic: subst h₂₃
Cleared hypotheses: p₃, h₂₃
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
⊢ Cochain.comp (G := mappingCocone φ) (liftCochain φ α β h) (snd φ) ⋯ = β
have h₁ : ∀ (p q : ℤ) (hpq : p + m = q),
  (Cochain.comp (G := mappingCocone φ) (liftCochain φ α β h) (snd φ) sorry).v p q hpq = β.v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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'
⊢ δ 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')
have dsimp : δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n sorry) =
  HSub.hSub (α := Cochain M (mappingCocone φ) n')
    ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) sorry)
    ((δ m n β + α.comp (Cochain.ofHom φ) sorry).comp
      (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')
Tactic: dsimp [liftCochain, inl, inr]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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'
⊢ δ 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')
have h₁ : ∀ (p q : ℤ) (hpq : p + n' = q),
  Cochain.v (δ n n' (Cochain.rightShift (mappingCone.liftCochain φ α β h) (-1) n sorry)) p q hpq =
    (HSub.hSub (α := Cochain M (mappingCocone φ) n')
          ((δ n n' α).comp (Cochain.rightShift (mappingCone.inl φ) (-1) 0 snd._proof_1) sorry)
          ((δ m n β + α.comp (Cochain.ofHom φ) sorry).comp
            (Cochain.rightShift (Cochain.ofHom (mappingCone.inr φ)) (-1) 1 inr._proof_2) hn')).v
      p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone (goal)
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
⊢ 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
have h₁ : HAdd.hAdd (α := M.X p ⟶ (mappingCocone φ).X q)
    ((δ n n' α).v p q hpq ≫ Cochain.v (mappingCone.inl φ) q (q + -1) sorry : 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) sorry ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
      (-α.v p (q + -1) sorry ≫ φ.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) sorry : 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) sorry ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q)
      (α.v p (q + -1) sorry ≫ φ.f (q + -1) ≫ Hom.f (mappingCone.inr φ) (q + -1) : M.X p ⟶ (mappingCocone φ).X q))
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)]