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
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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
rw : p + n = p' + a
rw₁ : p + (n' + a) = p' + a
⊢ q = p' + a
have rw₂ : p + n' + a = p' + a
Tactic: rw [← hpq, ← hn, ← add_assoc, hp']
-- 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 : ℤ
γ_1 γ₁ γ₂ : Cochain K L n_1
n' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
rw : p + n = p' + a
rw₁ : p + (n' + a) = p' + a
rw₂ : p + n' + a = p' + a
⊢ q = p' + a
have rw₃ : p' + a = p' + a
Tactic: rw [← hpq, ← hn, ← add_assoc, hp']
-- 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' a : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ (γ.rightUnshift n hn).v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a p' q ⋯).hom
have subst : (γ.rightUnshift n hn).v p q hpq = γ.v p (p + n') sorry ≫ (L.shiftFunctorObjXIso a (p + n') q sorry).hom
Tactic: subst hp'
Cleared hypotheses: p', hp'
-- 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' a : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯
have obtain : ∀ (hp' : p - a + n' = q),
  (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p sorry).inv ≫ γ.v (p - a) q sorry
Tactic: obtain rfl : p' = p - a := by lia
Cleared hypotheses: p', hp'
-- 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ p' + n = q'
have rw : p + a + n = q'
Tactic: rw [hp', hq', ← hpq, 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
⊢ p' + n = q'
have rw₁ : p + a + n = q + a
Tactic: rw [hp', hq', ← hpq, 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
rw₁ : p + a + n = q + a
⊢ p' + n = q'
have rw₂ : p + a + n = p + n + a
Tactic: rw [hp', hq', ← hpq, 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
rw₁ : p + a + n = q + a
rw₂ : p + a + n = p + n + a
⊢ p' + n = q'
have rw₃ : p + (a + n) = p + n + a
Tactic: rw [hp', hq', ← hpq, 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
rw₁ : p + a + n = q + a
rw₂ : p + a + n = p + n + a
rw₃ : p + (a + n) = p + n + a
⊢ p' + n = q'
have rw₄ : p + (n + a) = p + n + a
Tactic: rw [hp', hq', ← hpq, 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 p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
rw : p + a + n = q'
rw₁ : p + a + n = q + a
rw₂ : p + a + n = p + n + a
rw₃ : p + (a + n) = p + n + a
rw₄ : p + (n + a) = p + n + a
⊢ p' + n = q'
have rw₅ : p + (n + a) = p + (n + a)
Tactic: rw [hp', hq', ← hpq, 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 : CochainComplex.{v, u, 0} C ℤ
n : ℤ
γ : Cochain K L n
a p q : ℤ
hpq : p + n = q
p' q' : ℤ
hp' : p' = p + a
hq' : q' = q + a
⊢ (γ.shift a).v p q hpq = (K.shiftFunctorObjXIso a p p' hp').hom ≫ γ.v p' q' ⋯ ≫ (L.shiftFunctorObjXIso a q q' hq').inv
have subst : (γ.shift a).v p q hpq =
  (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (q + a) sorry ≫ (L.shiftFunctorObjXIso a q (q + a) sorry).inv
Tactic: subst hp' hq'
Cleared hypotheses: p', q', hp', hq'
-- 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').rightUnshift n hn' = γ
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((γ.rightShift a n' hn').rightUnshift n hn').v p q hpq = γ.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 ℤ
a n' : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn' : n' + a = n
⊢ (γ.rightUnshift n hn').rightShift a n' hn' = γ
have h : ∀ (p q : ℤ) (hpq : p + n' = q), ((γ.rightUnshift n hn').rightShift a n' hn').v p q hpq = γ.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'
⊢ (γ.leftShift a n' hn').leftUnshift n hn' = γ
have h : ∀ (p q : ℤ) (hpq : p + n = q), ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.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').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h : (a * n' + a * (a - 1) / 2).negOnePow •
    (K.shiftFunctorObjXIso a (q - n') p sorry).inv ≫ (γ.leftShift a n' hn').v (q - n') q sorry =
  γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₁ : (a * n' + a * (a - 1) / 2).negOnePow •
    (K.shiftFunctorObjXIso a (q - n') p sorry).inv ≫
      ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p sorry).hom ≫ γ.v p q hpq) =
  γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₂ : (a * n' + a * (a - 1) / 2).negOnePow •
    (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p sorry).inv ≫ (K.shiftFunctorObjXIso a (q - n') p sorry).hom ≫ γ.v p q hpq =
  γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq =
    γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₃ : (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq =
    γ.v p q hpq
h₃ : (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q hpq = γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq =
    γ.v p q hpq
h₃ : (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq
h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q hpq = γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₅ : HSMul.hSMul (α := ℤˣ) 1 (γ.v p q hpq) = γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (K.shiftFunctorObjXIso a (q - n') p ⋯).hom ≫ γ.v p q hpq =
    γ.v p q hpq
h₃ : (a * n' + a * (a - 1) / 2).negOnePow • (a * n' + a * (a - 1) / 2).negOnePow • γ.v p q hpq = γ.v p q hpq
h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q hpq = γ.v p q hpq
h₅ : HSMul.hSMul (α := ℤˣ) 1 (γ.v p q hpq) = γ.v p q hpq
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq
have h₆ : γ.v p q hpq = γ.v p q hpq
Tactic: rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),
    γ.leftShift_v a n' hn' (q - n') q (by lia) p hpq, Linear.comp_units_smul,
    Iso.inv_hom_id_assoc, smul_smul, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
⊢ (γ.leftUnshift n hn').leftShift a n' hn' = γ
have h : ∀ (p q : ℤ) (hpq : p + n' = q), ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h : (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) sorry).hom ≫ (γ.leftUnshift n hn').v (q - n) q sorry =
  γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₁ : (a * n' + a * (a - 1) / 2).negOnePow •
    (K.shiftFunctorObjXIso a p (q - n) sorry).hom ≫
      ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) sorry).inv ≫ γ.v p q sorry) =
  γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯) =
    γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₂ : (a * n' + a * (a - 1) / 2).negOnePow •
    (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) sorry).hom ≫ (K.shiftFunctorObjXIso a p (q - n) sorry).inv ≫ γ.v p q sorry =
  γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₃ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) •
    (K.shiftFunctorObjXIso a p (q - n) sorry).hom ≫ (K.shiftFunctorObjXIso a p (q - n) sorry).inv ≫ γ.v p q sorry =
  γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
h₃ :
  ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q sorry = γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, 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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
h :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
h₁ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫
        ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯) =
    γ.v p q hpq
h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow •
      (a * n' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
h₃ :
  ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (K.shiftFunctorObjXIso a p (q - n) ⋯).inv ≫ γ.v p q ⋯ =
    γ.v p q hpq
h₄ : ((a * n' + a * (a - 1) / 2).negOnePow * (a * n' + a * (a - 1) / 2).negOnePow) • γ.v p q ⋯ = γ.v p q hpq
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq
have h₅ : HSMul.hSMul (α := ℤˣ) 1 (γ.v p q sorry) = γ.v p q hpq
Tactic: rw [(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),
    γ.leftUnshift_v n hn' (q - n) q (by lia) p hpq, Linear.comp_units_smul, smul_smul,
    Iso.hom_inv_id_assoc, Int.units_mul_self, one_smul]