-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma leftShift_comp (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : Cochain L M m)
    (h : n + m = t) (ht' : t + a = t') :
    (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ'
      (by rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc])

Proof state:
case h.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow

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

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Tactic:
have h' : n' + m = t' := by omega

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

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

Result:
no goals

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

Result:
no goals

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

Result:
no goals

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

Result:
case h.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow

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

Result:
no goals

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

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = (a * m).negOnePow • ((γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex 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'
⊢ ((γ.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 omega),
  γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by omega),
  (γ.comp γ' h).leftShift_v a t' (by omega) p q hpq (p + a) (by omega),
  smul_smul, Linear.units_smul_comp, assoc, Int.negOnePow_add, ← mul_assoc, ← h',
  comp_v _ _ h (p + a) (p + n') q (by omega) (by omega)]

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

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex 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'
⊢ n' + m = t'

Tactic:
rw [← ht', ← h, ← hn', add_assoc, add_comm a, add_assoc]

Result:
no goals