-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma map_opShiftFunctorEquivalence_counitIso_inv_app_unop (X : Cᵒᵖ) (n : ℤ) :
    F.map ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
      ((F.op.commShiftIso n).inv.app (op (X.unop⟦n⟧))).unop ≫
        (((F.commShiftIso n).hom.app X.unop).op⟦n⟧').unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj X.unop))).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 (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op).unop ≫
          ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((F.op.commShiftIso n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
dsimp

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 (𝟙 (unop X)) =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op).unop ≫
          ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((F.op.commShiftIso n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).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 ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
    ((F.op.commShiftIso n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
      ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (unop X)).op).unop ≫
        ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
rw [← cancel_epi (F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop),
  ← F.map_comp, ← unop_comp, Iso.inv_hom_id_app,
  map_opShiftFunctorEquivalence_counitIso_hom_app_unop]

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 (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op).unop ≫
          ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((F.op.commShiftIso n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).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.obj (unop X)) =
    ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X))) ≫
        (shiftFunctor Dᵒᵖ n).map (𝟙 ((F ⋙ shiftFunctor D n).obj (unop X))).op ≫
          (opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
simp

Result:
no goals

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 (𝟙 (unop X)) =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op).unop ≫
          ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((F.op.commShiftIso n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
simp only [map_id, assoc, Iso.unop_hom_inv_id_app_assoc, ← Functor.map_comp_assoc,
  ← unop_comp, Iso.inv_hom_id_app_assoc, ← unop_comp_assoc, ← op_comp,
  Iso.inv_hom_id_app]

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.obj (unop X)) =
    ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X))) ≫
        (shiftFunctor Dᵒᵖ n).map (𝟙 ((F ⋙ shiftFunctor D n).obj (unop X))).op ≫
          (opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop