-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma δ_rightShift (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m) :
    δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Proof state:
case pos.h.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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.negOnePow * m.negOnePow

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

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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:
omega

Result:
no goals

Proof state:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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:
congr 1

Result:
case pos.h.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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.negOnePow * m.negOnePow

Proof state:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').v p q hpq

Tactic:
dsimp

Result:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
by_cases hnm : n + 1 = m

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Proof state:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj 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]

Result:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
x✝ : n' + 1 = m'
⊢ n + 1 = m

Tactic:
omega

Result:
no goals

Proof state:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = a.negOnePow • ((δ n m γ).rightShift a m' hm').v p q hpq

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 omega) rfl,
  δ_v n' m' hnm' _ p q hpq (p+n') (p+1) (by omega) rfl,
  γ.rightShift_v a n' hn' p (p+n') rfl (p+n) rfl,
  γ.rightShift_v a n' hn' (p+1) q _ (p+m) (by omega)]

Result:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') (p + n) ⋯).inv) ≫
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj 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

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
have hnm' : n' + 1 = m' := by omega

Result:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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:
omega

Result:
no goals

Proof state:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
ext p q hpq

Result:
case pos.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (δ n' m' (γ.rightShift a n' hn')).v p q hpq = (a.negOnePow • (δ n m γ).rightShift a m' hm').v p q hpq