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 m : ℤ
hnm : ¬n + 1 = m
neg : 0 = a.negOnePow • (δ n m γ).shift a
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have neg₁ : 0 =
  HSMul.hSMul (β :=
    Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
    a.negOnePow (shift 0 a)
Tactic: rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_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 : ℤ
γ : Cochain K L n
a m : ℤ
hnm : ¬n + 1 = m
neg : 0 = a.negOnePow • (δ n m γ).shift a
neg₁ :
  0 =
    HSMul.hSMul (β :=
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
      a.negOnePow (shift 0 a)
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have neg₂ : 0 =
  HSMul.hSMul (β :=
    Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
    a.negOnePow 0
Tactic: rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_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 : ℤ
γ : Cochain K L n
a m : ℤ
hnm : ¬n + 1 = m
neg : 0 = a.negOnePow • (δ n m γ).shift a
neg₁ :
  0 =
    HSMul.hSMul (β :=
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
      a.negOnePow (shift 0 a)
neg₂ :
  0 =
    HSMul.hSMul (β :=
      Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
      a.negOnePow 0
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have neg₃ : Eq.{v + 1} (α :=
  Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K)
    (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m)
  0 0
Tactic: rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a
have h : ∀ (p q : ℤ) (hpq : p + n = q),
  ((γ.rightShift a n' hn').leftShift a n hn').v p q hpq = ((a * n + a * (a - 1) / 2).negOnePow • γ.shift a).v 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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ ((γ.rightShift a n' hn').leftShift a n hn').v p q hpq = ((a * n + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq
have h : (a * n + a * (a - 1) / 2).negOnePow •
    (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (q + a) sorry ≫ (L.shiftFunctorObjXIso a q (q + a) sorry).inv =
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: simp only [leftShift_v _ a n hn' p q hpq (p + a) (by lia),
    rightShift_v _ a n' hn' (p + a) q (by lia) (q + a) (by lia), units_smul_v, shift_v']
-- 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' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h : (a * n + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) sorry ≫ 𝟙 (L.X (q + a)) =
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: dsimp
-- 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' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h : (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry ≫ 𝟙 (L.X (q + a)) =
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: rw [id_comp, comp_id]
-- 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' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
h :
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
⊢ (a * n + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯ ≫ 𝟙 (L.X (q + a)) =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry =
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: rw [id_comp, comp_id]
-- 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' : ℤ
hn' : n + a = n'
⊢ (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a
have h : ∀ (p q : ℤ) (hpq : p + n = q),
  ((γ.leftShift a n' hn').rightShift a n hn').v p q hpq = ((a * n' + a * (a - 1) / 2).negOnePow • γ.shift a).v 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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((γ.leftShift a n' hn').rightShift a n hn').v p q hpq = ((a * n' + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq
have h : ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (q + a) sorry) ≫
    (L.shiftFunctorObjXIso a q (q + a) sorry).inv =
  (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: simp only [rightShift_v _ a n hn' p q hpq (q + a) (by lia),
    leftShift_v _ a n' hn' p (q + a) (by lia) (p + a) (by lia), units_smul_v, shift_v']
-- 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯) ≫
      (L.shiftFunctorObjXIso a q (q + a) ⋯).inv =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h : ((a * n' + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) sorry) ≫ 𝟙 (L.X (q + a)) =
  (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: dsimp
-- 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯) ≫ 𝟙 (L.X (q + a)) =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h : ((a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry) ≫ 𝟙 (L.X (q + a)) =
  (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: rw [id_comp, comp_id]
-- 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  ((a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯) ≫ 𝟙 (L.X (q + a)) =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • 𝟙 (K.X (p + a)) ≫ γ.v (p + a) (q + a) ⋯) ≫ 𝟙 (L.X (q + a)) =
    (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
have h₁ : (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry =
  (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) sorry
Tactic: rw [id_comp, comp_id]
-- 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''
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
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''
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₁ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = a.negOnePow • (a * n'' + 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
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₂ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * n'' + 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
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₃ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * (n + a) + 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
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₄ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a = (a.negOnePow * (a * (a + n) + 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
⊢ (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn''
have rw₅ : (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
  (a.negOnePow * (a * a + a * n + 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
⊢ (γ.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 * a + a * n + 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
⊢ (γ.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 * 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
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
⊢ (γ.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 * 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
⊢ (γ.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]