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 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'
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 γ' ⋯).v p q hpq
⊢ (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯

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 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
⊢ n' + m = t'

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 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
⊢ n' + m = t'

Tactic:
have h' : n' + m = t' := 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 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₁ : ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).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 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'
⊢ p + n' + m = 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 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'
⊢ p + a + n = p + n'

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 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'
⊢ t + a = t'

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 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'
⊢ p + a + t = 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 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 * (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 ⋯
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

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)]

Premises used: CategoryTheory.Category.assoc, CochainComplex.HomComplex.Cochain.comp, CochainComplex.HomComplex.Cochain.comp_v, CategoryTheory.Linear.units_smul_comp, mul_assoc, smul_smul, Int.negOnePow_add, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow
⊢ ((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 ⋯

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 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
h₃ h₄ : (a * m).negOnePow * (a * n').negOnePow = (a * m).negOnePow * (a * n').negOnePow
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow

Tactic:
rw [add_comm n', mul_add, Int.negOnePow_add]

Premises used: Int.negOnePow_add, add_comm, mul_add
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
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 γ' ⋯
rw₃ rw₄ : (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]

Premises used: CochainComplex.HomComplex.Cochain.leftShift_comp, one_smul, MulZeroClass.mul_zero, Int.negOnePow_zero, add_zero
-- 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
pos : ∀ (hnm : n + 1 = m), δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
neg : ∀ (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'

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 n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : 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' := 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'
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
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

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' 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' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').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 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
⊢ p + n = p + m - 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 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
⊢ p + n' = q - 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 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
⊢ p + 1 + n = p + 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
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
pos :
  (γ.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
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq

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)]

Premises used: CochainComplex.HomComplex.δ_v, CochainComplex.HomComplex.δ, HAdd.hAdd, OfNat.ofNat, CochainComplex.HomComplex.Cochain.rightShift_v, 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 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 :
  m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv =
    (a.negOnePow * m.negOnePow) • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv
⊢ (γ.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

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Linear.units_smul_comp, smul_smul, CategoryTheory.Linear.comp_units_smul, CochainComplex.shiftFunctorObjXIso, CategoryTheory.Preadditive.add_comp, HomologicalComplex.XIsoOfEq_inv_comp_d, CochainComplex.shiftFunctor_obj_d', HomologicalComplex.d_comp_XIsoOfEq_inv, add_right_inj, smul_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
⊢ m'.negOnePow • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv =
    (a.negOnePow * m.negOnePow) • K.d p (p + 1) ≫ γ.v (p + 1) (p + m) ⋯ ≫ (HomologicalComplex.XIsoOfEq L ⋯).inv

Tactic:
simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc,
      Int.units_mul_self, one_mul]

Premises used: mul_assoc, Int.negOnePow_add, add_comm, 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
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 γ).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
neg₃ neg₄ :
  Eq.{v + 1} (α := Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) m') 0 0
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

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

Premises used: smul_zero, CochainComplex.HomComplex.Cochain.rightShift_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 K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) a) L) n'
n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
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')
⊢ δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

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

Premises used: AddEquiv.surjective, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv, 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 ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'
⊢ δ 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:
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 ((γ'.rightShift a n' hn).rightUnshift n hn) = a.negOnePow • (δ n' m' (γ'.rightShift a n' hn)).rightUnshift m hm'

Tactic:
simp only [rightUnshift_rightShift, γ'.δ_rightShift a n' m' hn m hm', rightUnshift_units_smul,
    smul_smul, Int.units_mul_self, one_smul]

Premises used: CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, smul_smul, one_smul, CochainComplex.HomComplex.Cochain.δ_rightShift, CochainComplex.HomComplex.Cochain.rightUnshift_rightShift, 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'
pos : ∀ (hnm : n + 1 = m), δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'
neg : ∀ (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'

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 n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : 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' := 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'
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
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

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' 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' m' (γ.leftShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).leftShift a m' hm').v p q hpq
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).leftShift a m' hm').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 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
⊢ p + a + m = 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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + n' = q - 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 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
⊢ 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 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
⊢ p + a + n = p + n'

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
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + 1 + 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' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ p + 1 + 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' 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 • (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 ⋯))
⊢ (δ n' m' (γ.leftShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).leftShift a m' hm').v p q hpq

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)]

Premises used: CochainComplex.HomComplex.δ_v, CochainComplex.HomComplex.δ, HAdd.hAdd, CochainComplex.HomComplex.Cochain.leftShift_v, OfNat.ofNat, rfl