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

Proof state:
C : Type u_1
inst✝² : Category.{?u.83805, 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
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
⊢ (up ℤ).π (up ℤ) (up ℤ) (a', b) = n'

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{?u.83805, 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
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
⊢ a' + b = n'

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

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 ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q (n + x) ⋯) =
    𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x))

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 ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n =
    (K.shiftFunctor₁XXIso a x (a + x) ⋯ b).hom ≫
      K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).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 ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
⊢ (((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq => K.ιTotal (up ℤ) (p + x) q (n + x) ⋯) =
    𝟙 ((K.X (a + x)).X b) ≫ K.ιTotal (up ℤ) (a + x) b (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x))

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

Tactic:
subst ha' hn'

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