awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a
rw₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₃ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₄ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₅ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₆ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₇ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₈ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₉ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₁₀ : ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
  (a.negOnePow * (a.negOnePow * (a * n).negOnePow) * (a * (a - 1) / 2).negOnePow) • γ.shift a
Tactic: rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
    Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
    ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a
rw₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₃ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₄ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₅ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₆ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₇ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₈ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₉ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₁₀ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow) * (a * (a - 1) / 2).negOnePow) • γ.shift a
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₁₁ : ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
  (a.negOnePow * a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
Tactic: rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
    Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
    ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a
rw₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₃ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₄ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₅ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₆ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₇ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₈ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₉ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₁₀ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow) * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₁ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₁₂ : ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
  (1 * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
Tactic: rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
    Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
    ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + a * (a - 1) / 2).negOnePow • γ.shift a
rw₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₃ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (n + a) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₄ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * (a + n) + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₅ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₆ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
rw₇ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₈ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₉ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
rw₁₀ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a.negOnePow * (a * n).negOnePow) * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₁ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * a.negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
rw₁₂ :
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (1 * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₁₃ : ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
  ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a
Tactic: rw [leftShift_rightShift, rightShift_leftShift, smul_smul, ← hn'', add_comm n a, mul_add,
    Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_add, Int.negOnePow_mul_self,
    ← mul_assoc, ← mul_assoc, Int.units_mul_self, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n').rightUnshift n hn)) 0
have rw : a.negOnePow •
    Cochain.rightUnshift
      (δ n' (n + 1 - a) (↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')) (n + 1) sorry =
  0
Tactic: rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
rw :
  a.negOnePow •
      Cochain.rightUnshift
        (δ n' (n + 1 - a) (↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')) (n + 1) ⋯ =
    0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n').rightUnshift n hn)) 0
have rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.rightUnshift (n' := n + 1 - a) 0 (n + 1) sorry) = 0
Tactic: rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
rw :
  a.negOnePow •
      Cochain.rightUnshift
        (δ n' (n + 1 - a) (↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')) (n + 1) ⋯ =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.rightUnshift (n' := n + 1 - a) 0 (n + 1) ⋯) = 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n').rightUnshift n hn)) 0
have rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
Tactic: rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
rw :
  a.negOnePow •
      Cochain.rightUnshift
        (δ n' (n + 1 - a) (↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')) (n + 1) ⋯ =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.rightUnshift (n' := n + 1 - a) 0 (n + 1) ⋯) = 0
rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n').rightUnshift n hn)) 0
have rw₃ : Eq.{v + 1} (α := Cochain K L (n + 1)) 0 0
Tactic: rw [Cochain.δ_rightUnshift _ n hn (n + 1) (n + 1 - a) (by lia),
      δ_eq_zero, Cochain.rightUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n').leftUnshift n hn)) 0
have rw : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow
    (Cochain.leftUnshift
      (δ n' (n + 1 + a) (↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')) (n + 1) sorry) =
  0
Tactic: rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,
      δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
rw :
  HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow
      (Cochain.leftUnshift
        (δ n' (n + 1 + a) (↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')) (n + 1) ⋯) =
    0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n').leftUnshift n hn)) 0
have rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.leftUnshift (n' := n + 1 + a) 0 (n + 1) sorry) = 0
Tactic: rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,
      δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
rw :
  HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow
      (Cochain.leftUnshift
        (δ n' (n + 1 + a) (↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')) (n + 1) ⋯) =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.leftUnshift (n' := n + 1 + a) 0 (n + 1) ⋯) = 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n').leftUnshift n hn)) 0
have rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
Tactic: rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,
      δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L M : CochainComplex.{v, u, 0} C ℤ
n_1 n' a : ℤ
γ : Cocycle (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
rw :
  HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow
      (Cochain.leftUnshift
        (δ n' (n + 1 + a) (↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')) (n + 1) ⋯) =
    0
rw₁ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow (Cochain.leftUnshift (n' := n + 1 + a) 0 (n + 1) ⋯) = 0
rw₂ : HSMul.hSMul (β := Cochain K L (n + 1)) a.negOnePow 0 = 0
⊢ Eq (α := Cochain K L (n + 1))
    (δ n (n + 1) ((↑γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n').leftUnshift n hn)) 0
have rw₃ : Eq.{v + 1} (α := Cochain K L (n + 1)) 0 0
Tactic: rw [Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,
      δ_eq_zero, Cochain.leftUnshift_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
K' : CochainComplex.{v, u, 0} C ℤ
g : K' ⟶ K
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
⊢ Eq (α := Cocycle K' L n)
    ((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n) (g ≫ f) :
      Cocycle K' L n)
    (precomp ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
        g :
      Cocycle K' L n)
have h : ∀ (p q : ℤ) (hpq : p + n = q),
  Eq (α := K'.X p ⟶ L.X q)
    (Cochain.v
      (↑((equivHomShift : (a : K' ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K' L n)
            (g ≫ f)) :
        Cochain K' L n)
      p q hpq)
    (Cochain.v
      (↑(precomp
            ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
            g) :
        Cochain K' L n)
      p q hpq)
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
f : K ⟶ Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L
L' : CochainComplex.{v, u, 0} C ℤ
g : L ⟶ L'
⊢ Eq (α := Cocycle K L' n)
    ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
        (f ≫ CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g) :
      Cocycle K L' n)
    (postcomp ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
        g :
      Cocycle K L' n)
have h : ∀ (p : ℤ),
  Eq (α := K.X p ⟶ L'.X (p + n))
    (Cochain.v
      (↑((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L') → Cocycle K L' n)
            (f ≫ CategoryTheory.Functor.map (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) g)) :
        Cochain K L' n)
      p (p + n) sorry)
    (Cochain.v
      (↑(postcomp
            ((equivHomShift : (a : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) → Cocycle K L n) f)
            g) :
        Cochain K L' n)
      p (p + n) sorry)
Tactic: ext p q rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')
have pos : ∀ (hq : q + 1 = q'),
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')
Tactic: by_cases hq : q + 1 = q'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
pos :
  ∀ (hq : q + 1 = q'),
    Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
      (fromSingleMk (f ≫ K.d q q') h')
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')
have neg : ∀ (hq : ¬q + 1 = q'),
  Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n') (δ n n' (fromSingleMk f h))
    (fromSingleMk (f ≫ K.d q q') h')
Tactic: by_cases hq : q + 1 = q'
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ Eq (α := Cochain (Functor.obj (singleFunctor C p) X) K n')
    (δ n n' (single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f) n))
    (single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f ≫ K.d q q') n')
have pos : single ((Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f) ≫ K.d q q') n' +
    HSMul.hSMul (β := Cochain (Functor.obj (singleFunctor C p) X) K n') n'.negOnePow
      (single (p := p - 1)
        (HomologicalComplex.d (Functor.obj (singleFunctor C p) X) (p - 1) p ≫
          Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f)
        n') =
  single (Iso.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ f ≫ K.d q q') n'
Tactic: rw [δ_single _ n n' (by lia) (p - 1) q' (by lia) hq]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
K : CochainComplex.{v, u, 0} C ℤ
p q n : ℤ
h : p + n = q
α : Cochain (Functor.obj (singleFunctor C p) X) K n
⊢ (fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
      ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
          Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
        α) =
    α
have h₁ : ∀ (p' q' : ℤ) (hpq' : p' + n = q'),
  v
      ((fun (f : X ⟶ K.X q) ↦ (fromSingleMk f h : Cochain (Functor.obj (singleFunctor C p) X) K n))
        ((fun (α : Cochain (Functor.obj (singleFunctor C p) X) K n) ↦
            Iso.inv (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X) ≫ α.v p q h)
          α))
      p' q' hpq' =
    α.v p' q' hpq'
Tactic: ext p' q' hpq'