-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma δ_shift (a m : ℤ) :
    δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

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

Tactic:
simp only [shift_v', sub_add_cancel, 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 omega) (q - 1 + a) (p + 1 + a)
    (by omega) (by omega),
  smul_add, Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj]

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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow • a.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex 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:
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 m : ℤ
hnm : n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

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

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

Result:
no goals

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

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

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

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

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

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

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

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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow • a.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯

Tactic:
rw [smul_comm]

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 m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ p + a + m = q + a

Tactic:
omega

Result:
no goals