-- Mathlib/Algebra/Homology/TotalComplexShift.lean
@[reassoc]
lemma ι_totalShift₂Iso_hom_f (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y)
    (n' : ℤ) (hn' : n' = n + y) :
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
      (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' (by dsimp; omega) ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv

Tactic:
dsimp [totalShift₂Iso, totalShift₂XIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq => (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) (n + y) ⋯) =
    (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq => (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) (n + y) ⋯) =
    (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))

Tactic:
simp only [ι_totalDesc, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv

Tactic:
subst hb' hn'

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv

Proof state:
C : Type u_1
inst✝² : Category.{?u.211397, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ a + b' = n'

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{?u.211397, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ (up ℤ).π (up ℤ) (up ℤ) (a, b') = n'

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{?u.211397, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ a + b' = n'