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

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      (total.map f (up ℤ)).f (n + y)

Tactic:
rw [id_comp, id_comp, comp_id, comp_id, Linear.comp_units_smul,
  Linear.units_smul_comp, ι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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ)).f n ≫ (L.totalShift₂Iso y).hom.f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)

Tactic:
rw [ιTotal_map_assoc, L.ι_totalShift₂Iso_hom_f y i₁ i₂ n h _ rfl _ rfl,
  K.ι_totalShift₂Iso_hom_f_assoc y 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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((i₁ * y).negOnePow •
        (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫
      (total.map f (up ℤ)).f (n + y)

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom).f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ)).f n ≫ (L.totalShift₂Iso y).hom.f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom =
    (K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : (up ℤ).π (up ℤ) (up ℤ) (i₁, i₂) = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom).f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      ((K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((i₁ * y).negOnePow •
        (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫
      (total.map f (up ℤ)).f (n + y)

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f i₁).f (i₂ + y) ≫
      ((i₁ * y).negOnePow •
        𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) =
    ((i₁ * y).negOnePow •
        𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫
      (total.map f (up ℤ)).f (n + y)