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' 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')
neg₂ :
  0 =
    HSMul.hSMul (β := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m')
      a.negOnePow 0
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
have neg₃ : Eq.{v + 1} (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m') 0 0
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 ℤ
a n' : ℤ
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
⊢ δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'
have obtain : ∀ (γ' : Cochain K L n),
  δ n m
      (rightUnshift
        ((rightShiftAddEquiv K L n a n' hn :
            (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
          γ')
        n hn) =
    HSMul.hSMul (β := Cochain K L m) a.negOnePow
      (rightUnshift
        (δ n' m'
          ((rightShiftAddEquiv K L n a n' hn :
              (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
            γ'))
        m hm')
Tactic: obtain ⟨γ', rfl⟩ := (rightShiftAddEquiv K L n a n' hn).surjective γ
Cleared hypotheses: γ
-- 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' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m
      (rightUnshift
        ((rightShiftAddEquiv K L n a n' hn :
            (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
          γ')
        n hn) =
    HSMul.hSMul (β := Cochain K L m) a.negOnePow
      (rightUnshift
        (δ n' m'
          ((rightShiftAddEquiv K L n a n' hn :
              (a_1 : Cochain K L n) → Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n')
            γ'))
        m hm')
have dsimp : δ n m ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'
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'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have pos : ∀ (hnm : n + 1 = m), δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift 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' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have neg : ∀ (hnm : ¬n + 1 = m), δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift 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' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift 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' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have pos : ∀ (p q : ℤ) (hpq : p + m' = q),
  (δ n' m' (γ.leftShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).leftShift 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' (γ.leftShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).leftShift a m' hm').v p q hpq
have pos : (δ n' m' (γ.leftShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).leftShift 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' (γ.leftShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).leftShift a m' hm').v p q hpq
have pos : ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫ γ.v (p + a) (p + n') sorry) ≫
      L.d (p + n') q +
    m'.negOnePow •
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).d p (p + 1) ≫
        ((a * n' + a * (a - 1) / 2).negOnePow •
          (K.shiftFunctorObjXIso a (p + 1) (p + 1 + a) sorry).hom ≫ γ.v (p + 1 + a) q sorry) =
  a.negOnePow •
    (a * m' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (p + a) sorry).hom ≫
        (γ.v (p + a) (p + n') sorry ≫ L.d (p + n') q +
          HSMul.hSMul (β := K.X (p + a) ⟶ L.X q) m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q sorry))
Tactic: rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p + a) (by lia),
      δ_v n m hnm _ (p + a) q (by lia) (p + n') (p + 1 + a) (by lia) (by lia),
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
      γ.leftShift_v a n' hn' (p + 1) q (by lia) (p + 1 + a) (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
⊢ ((a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (p + n') ⋯) ≫
        L.d (p + n') q +
      m'.negOnePow •
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).d p (p + 1) ≫
          ((a * n' + a * (a - 1) / 2).negOnePow •
            (K.shiftFunctorObjXIso a (p + 1) (p + 1 + a) ⋯).hom ≫ γ.v (p + 1 + a) q ⋯) =
    a.negOnePow •
      (a * m' + a * (a - 1) / 2).negOnePow •
        (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫
          (γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
            HSMul.hSMul (β := K.X (p + a) ⟶ L.X q) m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯))
have pos : (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (p + n') sorry ≫ L.d (p + n') q +
    HSMul.hSMul (β := (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶ L.X q)
      (m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow))
      (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q sorry) =
  (a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow) • γ.v (p + a) (p + n') sorry ≫ L.d (p + n') q +
    HSMul.hSMul (β := K.X (p + a) ⟶ L.X q) (a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow))
      (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q sorry)
Tactic: simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
      Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d',
      Linear.comp_units_smul, smul_add, smul_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'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      HSMul.hSMul (β := (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶ L.X q)
        (m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow))
        (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯) =
    (a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow) • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      HSMul.hSMul (β := K.X (p + a) ⟶ L.X q) (a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow))
        (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)
have pos : (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * m' + a * (a - 1) / 2).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 : 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
pos : (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow
⊢ (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      HSMul.hSMul (β := (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶ L.X q)
        (m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow))
        (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯) =
    (a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow) • γ.v (p + a) (p + n') ⋯ ≫ L.d (p + n') q +
      HSMul.hSMul (β := K.X (p + a) ⟶ L.X q) (a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow))
        (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) q ⋯)
have pos₁ : m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
  a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.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 : 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
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow
have pos : (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a + a * n' + a * (a - 1) / 2).negOnePow
Tactic: rw [← hnm', add_comm n', mul_add, mul_one]
-- 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
⊢ m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
    a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow)
have pos : (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a)).negOnePow =
  (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))).negOnePow
Tactic: simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]
-- 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 + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a)).negOnePow =
    (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))).negOnePow
have pos : n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) = a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))
Tactic: congr 1
-- 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 + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) = a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))
have linarith : n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) < a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)) →
  -1 + (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) + 1 - (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)))) = 0
Tactic: linarith
-- 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
linarith :
  n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) < a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)) →
    -1 + (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) + 1 - (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)))) = 0
⊢ n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) = a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))
have linarith₁ : a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)) < n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) →
  -1 + (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1)) + 1 - (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a))) = 0
Tactic: linarith
-- 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' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift 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' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have neg : 0 = a.negOnePow • (δ n m γ).leftShift a m' hm'
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_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 γ).leftShift a m' hm'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have neg₁ : 0 =
  HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m')
    a.negOnePow (leftShift 0 a m' hm')
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_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 γ).leftShift a m' hm'
neg₁ :
  0 =
    HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m')
      a.negOnePow (leftShift 0 a m' hm')
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have neg₂ : 0 =
  HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m')
    a.negOnePow 0
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_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 γ).leftShift a m' hm'
neg₁ :
  0 =
    HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m')
      a.negOnePow (leftShift 0 a m' hm')
neg₂ :
  0 =
    HSMul.hSMul (β := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m')
      a.negOnePow 0
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
have neg₃ : Eq.{v + 1} (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m') 0 0
Tactic: rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_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 ℤ
a n' : ℤ
γ : Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L n'
n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
⊢ δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'
have obtain : ∀ (γ' : Cochain K L n),
  δ n m
      (leftUnshift
        ((leftShiftAddEquiv K L n a n' hn :
            (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
          γ')
        n hn) =
    HSMul.hSMul (β := Cochain K L m) a.negOnePow
      (leftUnshift
        (δ n' m'
          ((leftShiftAddEquiv K L n a n' hn :
              (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
            γ'))
        m hm')
Tactic: obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ
Cleared hypotheses: γ
-- 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' n : ℤ
hn : n + a = n'
m m' : ℤ
hm' : m + a = m'
γ' : Cochain K L n
⊢ δ n m
      (leftUnshift
        ((leftShiftAddEquiv K L n a n' hn :
            (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
          γ')
        n hn) =
    HSMul.hSMul (β := Cochain K L m) a.negOnePow
      (leftUnshift
        (δ n' m'
          ((leftShiftAddEquiv K L n a n' hn :
              (a_1 : Cochain K L n) → Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n')
            γ'))
        m hm')
have dsimp : δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'
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 m : ℤ
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have pos : ∀ (hnm : n + 1 = m), δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
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 m : ℤ
pos : ∀ (hnm : n + 1 = m), δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have neg : ∀ (hnm : ¬n + 1 = m), δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
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 m : ℤ
hnm : n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have pos : ∀ (p q : ℤ) (hpq : p + m = q), (δ n m (γ.shift a)).v p q hpq = (a.negOnePow • (δ n m γ).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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (γ.shift a)).v p q hpq = (a.negOnePow • (δ n m γ).shift a).v p q hpq
have pos : (δ n m (γ.shift a)).v p q hpq = a.negOnePow • ((δ n m γ).shift a).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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (γ.shift a)).v p q hpq = a.negOnePow • ((δ n m γ).shift a).v p q hpq
have pos : m.negOnePow •
    HSMul.hSMul (β :=
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L).X q)
      a.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) sorry) =
  a.negOnePow •
    HSMul.hSMul (β := K.X (p + a) ⟶ L.X (q + a)) m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) sorry)
Tactic: simp only [shift_v', shiftFunctor_obj_d',
      δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
      δ_v n m hnm _ (p + a) (q + a) (by lia) (q - 1 + a) (p + 1 + a)
        (by lia) (by lia),
      smul_add, Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj]
-- 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
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow •
      HSMul.hSMul (β :=
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L).X q)
        a.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯) =
    a.negOnePow •
      HSMul.hSMul (β := K.X (p + a) ⟶ L.X (q + a)) m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯)
have pos : a.negOnePow •
    HSMul.hSMul (β :=
      (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K).X p ⟶
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L).X q)
      m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) sorry) =
  a.negOnePow •
    HSMul.hSMul (β := K.X (p + a) ⟶ L.X (q + a)) m.negOnePow (K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) sorry)
Tactic: rw [smul_comm]
-- 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
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
have neg : 0 = a.negOnePow • (δ n m γ).shift a
Tactic: rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_zero, smul_zero]