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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
h :
  (γ.comp γ' hnm).v p (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₁ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
have h₂ : (γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry) ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom =
  γ.v p (p + n) sorry ≫ (γ'.rightUnshift m' hm').v (p + n) q sorry
Tactic: rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),
    γ'.rightUnshift_v m' hm' (p + n) q (by lia) (p + n + m) rfl, assoc]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
h :
  (γ.comp γ' hnm).v p (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₁ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₂ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ (γ'.rightUnshift m' hm').v (p + n) q ⋯
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
have h₃ : (γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry) ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom =
  γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom
Tactic: rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),
    γ'.rightUnshift_v m' hm' (p + n) q (by lia) (p + n + m) rfl, assoc]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
m a : ℤ
γ' : Cochain L (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) M) m
nm : ℤ
hnm : n + m = nm
nm' : ℤ
hnm' : nm + a = nm'
m' : ℤ
hm' : m + a = m'
p q : ℤ
hpq : p + nm' = q
h :
  (γ.comp γ' hnm).v p (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₁ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
h₂ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ (γ'.rightUnshift m' hm').v (p + n) q ⋯
h₃ :
  (γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯) ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom =
    γ.v p (p + n) ⋯ ≫ γ'.v (p + n) (p + n + m) ⋯ ≫ (M.shiftFunctorObjXIso a (p + n + m) q ⋯).hom
⊢ ((γ.comp γ' hnm).rightUnshift nm' hnm').v p q hpq = (γ.comp (γ'.rightUnshift m' hm') ⋯).v p q hpq
have h₄ : γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom =
  γ.v p (p + n) sorry ≫ γ'.v (p + n) (p + n + m) sorry ≫ (M.shiftFunctorObjXIso a (p + n + m) q sorry).hom
Tactic: rw [(γ.comp γ' hnm).rightUnshift_v nm' hnm' p q hpq (p + n + m) (by lia),
    γ.comp_v γ' hnm p (p + n) (p + n + m) rfl rfl,
    comp_v _ _ (show n + m' = nm' by lia) p (p + n) q (by lia) (by lia),
    γ'.rightUnshift_v m' hm' (p + n) q (by lia) (p + n + m) rfl, assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
⊢ n' + m = t'
have rw : n' + m = t + a
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
⊢ n' + m = t'
have rw₁ : n' + m = n + m + a
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
rw₁ : n' + m = n + m + a
⊢ n' + m = t'
have rw₂ : n + a + m = n + m + a
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
rw₁ : n' + m = n + m + a
rw₂ : n + a + m = n + m + a
⊢ n' + m = t'
have rw₃ : n + (a + m) = n + m + a
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
rw₁ : n' + m = n + m + a
rw₂ : n + a + m = n + m + a
rw₃ : n + (a + m) = n + m + a
⊢ n' + m = t'
have rw₄ : n + (m + a) = n + m + a
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
rw : n' + m = t + a
rw₁ : n' + m = n + m + a
rw₂ : n + a + m = n + m + a
rw₃ : n + (a + m) = n + m + a
rw₄ : n + (m + a) = n + m + a
⊢ n' + m = t'
have rw₅ : n + (m + a) = n + (m + a)
Tactic: rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
⊢ (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯
have h₁ : ∀ (p q : ℤ) (hpq : p + t' = q),
  ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' sorry).v p q hpq
Tactic: ext p q hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
have h' : n' + m = t'
Tactic: have h' : n' + m = t' := by lia
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
have h₁ : ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' sorry).v p q hpq
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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
have h₁ : ((a * (n' + m)).negOnePow * (a * (a - 1) / 2).negOnePow) •
    (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (p + n') sorry ≫ γ'.v (p + n') q sorry =
  ((a * m).negOnePow * (a * n').negOnePow * (a * (a - 1) / 2).negOnePow) •
    (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (p + n') sorry ≫ γ'.v (p + n') q sorry
Tactic: simp only [Cochain.comp_v _ _ h' p (p + n') q rfl (by lia),
    γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
    (γ.comp γ' h).leftShift_v a t' (by lia) p q hpq (p + a) (by lia),
    smul_smul, Linear.units_smul_comp, assoc, Int.negOnePow_add, ← mul_assoc, ← h',
    comp_v _ _ h (p + a) (p + n') q (by lia) (by lia)]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((a * (n' + m)).negOnePow * (a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯ ≫ γ'.v (p + n') q ⋯ =
    ((a * m).negOnePow * (a * n').negOnePow * (a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯ ≫ γ'.v (p + n') q ⋯
have h₁ : (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow
Tactic: congr 2
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow
have h₁ : (a * (m + n')).negOnePow = (a * m).negOnePow * (a * n').negOnePow
Tactic: rw [add_comm n', mul_add, Int.negOnePow_add]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
h₁ : (a * (m + n')).negOnePow = (a * m).negOnePow * (a * n').negOnePow
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow
have h₂ : (a * m + a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow
Tactic: rw [add_comm n', mul_add, Int.negOnePow_add]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
h₁ : (a * (m + n')).negOnePow = (a * m).negOnePow * (a * n').negOnePow
h₂ : (a * m + a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow
have h₃ : (a * m).negOnePow * (a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow
Tactic: rw [add_comm n', mul_add, Int.negOnePow_add]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
have rw : (a * 0).negOnePow • (γ.leftShift a n' hn').comp γ' sorry = (γ.leftShift a n' hn').comp γ' sorry
Tactic: rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
rw : (a * 0).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
have rw₁ : Int.negOnePow 0 • (γ.leftShift a n' hn').comp γ' sorry = (γ.leftShift a n' hn').comp γ' sorry
Tactic: rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
rw : (a * 0).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
rw₁ : Int.negOnePow 0 • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
have rw₂ : HSMul.hSMul (α := ℤˣ) 1 ((γ.leftShift a n' hn').comp γ' sorry) = (γ.leftShift a n' hn').comp γ' sorry
Tactic: rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]
-- 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 M : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
rw : (a * 0).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
rw₁ : Int.negOnePow 0 • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
rw₂ : HSMul.hSMul (α := ℤˣ) 1 ((γ.leftShift a n' hn').comp γ' ⋯) = (γ.leftShift a n' hn').comp γ' ⋯
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
have rw₃ : (γ.leftShift a n' hn').comp γ' sorry = (γ.leftShift a n' hn').comp γ' sorry
Tactic: rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]
-- 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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have pos : ∀ (hnm : n + 1 = m), δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
Tactic: by_cases hnm : n + 1 = m
-- 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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
pos : ∀ (hnm : n + 1 = m), δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have neg : ∀ (hnm : ¬n + 1 = m), δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
Tactic: by_cases hnm : n + 1 = m
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (hypothesis)
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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have hnm' : n' + 1 = m'
Tactic: have hnm' : n' + 1 = m' := by lia
-- 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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have pos : ∀ (p q : ℤ) (hpq : p + m' = q),
  (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').v p q hpq
have pos : (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq
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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq
have pos : (γ.v p (p + n) sorry ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) sorry).inv) ≫
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L).d (p + n') q +
    m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) sorry ≫ (L.shiftFunctorObjXIso a q (p + m) sorry).inv =
  a.negOnePow •
    (γ.v p (p + n) sorry ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) sorry) ≫
      (L.shiftFunctorObjXIso a q (p + m) sorry).inv
Tactic: rw [(δ n m γ).rightShift_v a m' hm' p q hpq _ rfl,
      δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by lia) rfl,
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.rightShift_v a n' hn' p (p + n') rfl (p + n) rfl,
      γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by lia)]
-- 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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L).d (p + n') q +
      m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + m) ⋯).inv =
    a.negOnePow •
      (γ.v p (p + n) ⋯ ≫ L.d (p + n) (p + m) + m.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯) ≫
        (L.shiftFunctorObjXIso a q (p + m) ⋯).inv
have pos : m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) sorry ≫ (HomologicalComplex.XIsoOfEq L sorry).inv =
  (a.negOnePow * m.negOnePow) • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) sorry ≫ (HomologicalComplex.XIsoOfEq L sorry).inv
Tactic: simp only [shiftFunctorObjXIso, shiftFunctor_obj_d',
      Linear.comp_units_smul, assoc, HomologicalComplex.XIsoOfEq_inv_comp_d,
      add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
      add_right_inj, smul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift (hypothesis)
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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have hnm' : ¬n' + 1 = m'
Tactic: have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
-- 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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have neg : 0 = a.negOnePow • (δ n m γ).rightShift a m' hm'
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
neg : 0 = a.negOnePow • (δ n m γ).rightShift a m' hm'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have neg₁ : 0 =
  HSMul.hSMul (β := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m')
    a.negOnePow (rightShift 0 a m' hm')
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
hnm' : ¬n' + 1 = m'
neg : 0 = a.negOnePow • (δ n m γ).rightShift a m' hm'
neg₁ :
  0 =
    HSMul.hSMul (β := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m')
      a.negOnePow (rightShift 0 a m' hm')
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have neg₂ : 0 =
  HSMul.hSMul (β := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m')
    a.negOnePow 0
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]