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

Proof state:
case 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 : ℤ
⊢ (F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop).op =
    (((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).op

Tactic:
dsimp [opShiftFunctorEquivalence]

Result:
case 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 : ℤ
⊢ (F.map
        ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (unop X) ≫
          ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop)).op =
    ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X))) ≫
        (shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op) ≫
      (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
        ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

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.hom.app 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

Tactic:
apply Quiver.Hom.op_inj

Result:
case 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 : ℤ
⊢ (F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop).op =
    (((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).op

Proof state:
case 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 : ℤ
⊢ (F.map
        ((shiftFunctorCompIsoId C n (-n) ⋯).inv.app (unop X) ≫
          ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop)).op =
    ((F.op.commShiftIso n).hom.app (op ((shiftFunctor C n).obj (unop X))) ≫
        (shiftFunctor Dᵒᵖ n).map ((F.commShiftIso n).inv.app (unop X)).op) ≫
      (shiftFunctorOpIso D n (-n) ⋯).hom.app (op ((shiftFunctor D n).obj (F.obj (unop X)))) ≫
        ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
rw [assoc, F.op_commShiftIso_hom_app_assoc _ _ _ (add_neg_cancel n), map_comp,
  map_shiftFunctorCompIsoId_inv_app_assoc, op_comp, op_comp_assoc, op_comp_assoc,
  NatTrans.naturality_assoc, op_map, Iso.inv_hom_id_app_assoc, Quiver.Hom.unop_op]

Result:
no goals