-- Mathlib/Algebra/Homology/TotalComplexShift.lean
@[reassoc]
lemma totalShift₁Iso_hom_naturality [L.HasTotal (up ℤ)] :
    total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
      (K.totalShift₁Iso x).hom ≫ (total.map f (up ℤ))⟦x⟧'

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom =
    (K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))

Tactic:
ext n i₁ i₂ h

Result:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom).f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))).f n

Proof state:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ) ≫ (L.totalShift₁Iso x).hom).f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₁Iso x).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) x).map (total.map f (up ℤ))).f n

Tactic:
dsimp at h ⊢

Result:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ)).f n ≫ (L.totalShift₁Iso x).hom.f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)

Proof state:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
dsimp

Result:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f (i₁ + x)).f i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x)) ≫ (total.map f (up ℤ)).f (n + x)

Proof state:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f (i₁ + x)).f i₂ ≫
      𝟙 ((L.X (i₁ + x)).X i₂) ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + x)) =
    𝟙 ((K.X (i₁ + x)).X i₂) ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x)) ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
rw [id_comp, id_comp, id_comp, comp_id, ιTotal_map]

Result:
no goals

Proof state:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ)).f n ≫ (L.totalShift₁Iso x).hom.f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
  K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]

Result:
case h.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫ (total.map f (up ℤ)).f (n + x)