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

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' : a + b' = n + y
⊢ b = b' - y

Tactic:
omega

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 n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ (K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      𝟙 ((K.total (up ℤ)).X (n + y)) ≫
        K.totalDesc fun p q hpq =>
          (p * y).negOnePow • eqToHom ⋯ ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    (a * y).negOnePow • eqToHom ⋯ ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a (b' - y) n h

Tactic:
simp only [id_comp, ι_totalDesc]

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 n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a (b' - y) y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a (b' - y) n h

Tactic:
dsimp [totalShift₂Iso, totalShift₂XIso, shiftFunctor₂XXIso, XXIsoOfEq]

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 n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ (K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      𝟙 ((K.total (up ℤ)).X (n + y)) ≫
        K.totalDesc fun p q hpq =>
          (p * y).negOnePow • eqToHom ⋯ ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    (a * y).negOnePow • eqToHom ⋯ ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a (b' - y) n h

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' : a + b' = n + y
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h

Tactic:
obtain rfl : b = b' - y := by omega

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 n b' : ℤ
hb' : a + b' = n + y
h : a + (b' - y) = n
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a (b' - y) y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a (b' - y) n h

Proof state:
C : Type u_1
inst✝² : Category.{?u.215805, 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' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ b' = b + y

Tactic:
omega

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' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ K.ιTotal (up ℤ) a b' n' hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h

Tactic:
subst 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
b' : ℤ
hb' : a + b' = n + y
⊢ K.ιTotal (up ℤ) a b' (n + y) hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h