awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 • γ.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 ⋯)
⊢ ((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 ⋯))

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]

Premises used: CategoryTheory.Linear.units_smul_comp, HomologicalComplex.XIsoOfEq_rfl, CochainComplex.shiftFunctor_obj_X, smul_smul, CategoryTheory.Linear.comp_units_smul, CochainComplex.shiftFunctorObjXIso, CochainComplex.shiftFunctor_obj_d', CategoryTheory.Iso.refl_hom, smul_add, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
pos₁ :
  m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
    a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.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 ⋯)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 + a * n' + a * (a - 1) / 2).negOnePow
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow

Tactic:
rw [← hnm', add_comm n', mul_add, mul_one]

Premises used: add_comm, mul_add, mul_one
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 + a * n' + a * (a - 1) / 2).negOnePow

Tactic:
simp only [Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]

Premises used: mul_assoc, Int.negOnePow_add, one_mul, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 :
  (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a)).negOnePow =
    (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))).negOnePow
⊢ m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
    a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow)

Tactic:
simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]

Premises used: Int.negOnePow_add
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 : n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) = a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))
⊢ (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:
congr 1
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
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
⊢ n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a) = a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))

Tactic:
linarith
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
h : n' + 1 = m'
⊢ n + 1 = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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' + 1 = m'

Tactic:
have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
neg₃ neg₄ :
  Eq.{v + 1} (α := Cochain (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) K) L m') 0 0
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

Tactic:
rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_zero, smul_zero]

Premises used: smul_zero, CochainComplex.HomComplex.Cochain.leftShift_zero, CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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'
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')
⊢ δ n m (γ.leftUnshift n hn) = a.negOnePow • (δ n' m' γ).leftUnshift m hm'

Tactic:
obtain ⟨γ', rfl⟩ := (leftShiftAddEquiv K L n a n' hn).surjective γ

Premises used: AddEquiv.surjective, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
dsimp :
  δ n m ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'
⊢ δ 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:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 ((γ'.leftShift a n' hn).leftUnshift n hn) = a.negOnePow • (δ n' m' (γ'.leftShift a n' hn)).leftUnshift m hm'

Tactic:
simp only [leftUnshift_leftShift, γ'.δ_leftShift a n' m' hn m hm', leftUnshift_units_smul,
    smul_smul, Int.units_mul_self, one_smul]

Premises used: smul_smul, one_smul, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, CochainComplex.HomComplex.Cochain.leftUnshift_leftShift, CochainComplex.HomComplex.Cochain.δ_leftShift, Int.units_mul_self
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
neg : ∀ (hnm : ¬n + 1 = m), δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
by_cases hnm : n + 1 = m
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
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
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
pos : (δ n m (γ.shift a)).v p q hpq = a.negOnePow • ((δ n m γ).shift a).v p q hpq
⊢ (δ n m (γ.shift a)).v p q hpq = (a.negOnePow • (δ n m γ).shift a).v p q hpq

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + a + m = q + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ q - 1 + a = q + a - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + a + 1 = p + 1 + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
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) ⋯) =
    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) ⋯)
⊢ (δ n m (γ.shift a)).v p q hpq = a.negOnePow • ((δ n m γ).shift a).v p q hpq

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]

Premises used: CochainComplex.HomComplex.δ_v, CategoryTheory.Linear.units_smul_comp, HSub.hSub, CategoryTheory.Linear.comp_units_smul, HAdd.hAdd, CochainComplex.shiftFunctor_obj_d', OfNat.ofNat, CochainComplex.HomComplex.Cochain.shift_v', add_right_inj, smul_add, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
pos 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) ⋯) =
    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) ⋯)
⊢ 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) ⋯)

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
neg₃ 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
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
rw [δ_shape _ _ hnm, δ_shape _ _ hnm, shift_zero, smul_zero]

Premises used: CochainComplex.HomComplex.Cochain.shift_zero, smul_zero, CochainComplex.HomComplex.δ_shape
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
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
⊢ (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + a + n' = q

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + a + n = q + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 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) ⋯
⊢ ((γ.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:
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']

Premises used: CochainComplex.HomComplex.Cochain.units_smul_v, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.shift_v'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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.X (p + a)) ≫ γ.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.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) ⋯

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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) ⋯
h₁ h₂ :
  (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (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) ⋯

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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'
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
⊢ (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
ext p q hpq
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + n' = q + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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
⊢ p + a + n = q + a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 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) ⋯
⊢ ((γ.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:
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']

Premises used: CochainComplex.HomComplex.Cochain.units_smul_v, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.shift_v'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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.X (p + a)) ≫ γ.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.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) ⋯

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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) ⋯
h₁ h₂ :
  (a * n' + a * (a - 1) / 2).negOnePow • γ.v (p + a) (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) ⋯

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp