-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma map_opShiftFunctorEquivalence_unitIso_hom_app_unop (X : Cᵒᵖ) (n : ℤ) :
    F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop =
      (F.commShiftIso n).hom.app _ ≫
        (((F.op).commShiftIso n).inv.app X).unop⟦n⟧' ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op _)).unop

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop ≫
        (shiftFunctorCompIsoId C (-n) n ⋯).hom.app (unop X)) =
    (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop ≫
        (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
          (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
simp only [map_comp, unop_comp, Quiver.Hom.unop_op, assoc,
  map_shiftFunctorCompIsoId_hom_app, commShiftIso_hom_naturality_assoc,
  op_commShiftIso_inv_app _ _ _ _ (add_neg_cancel n)]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map (F.map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop) ≫
        (shiftFunctor D n).map ((F.commShiftIso (-n)).hom.app (unop X)) ≫
          (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map (F.map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop) ≫
        (shiftFunctor D n).map ((F.commShiftIso (-n)).hom.app (unop X)) ≫
          (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
            (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
              (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Proof state:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
rw [map_id, id_comp]

Result:
no goals

Proof state:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
rw [← Functor.map_comp_assoc, ← unop_comp,
  Iso.inv_hom_id_app]

Result:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).op.obj (op (F.obj (unop X))))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map (F.map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop) ≫
        (shiftFunctor D n).map ((F.commShiftIso (-n)).hom.app (unop X)) ≫
          (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map (F.map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop) ≫
        (shiftFunctor D n).map ((F.commShiftIso (-n)).hom.app (unop X)) ≫
          (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
            (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
              (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
congr 3

Result:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
        (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).unitIso.hom.app X).unop =
    (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
dsimp [opShiftFunctorEquivalence]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop ≫
        (shiftFunctorCompIsoId C (-n) n ⋯).hom.app (unop X)) =
    (F.commShiftIso n).hom.app (unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      (shiftFunctor D n).map ((F.op.commShiftIso n).inv.app X).unop ≫
        (shiftFunctor D n).map ((shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop X)))).unop ≫
          (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Proof state:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).op.obj (op (F.obj (unop X))))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
dsimp

Result:
case e_a.e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))