awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
h : n + -n = 0
⊢ Eq (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)
    (NatTrans.app (Iso.hom (commShiftIso F.op n)) X)
    (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n (-n) h)) X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F (-n))) (unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) h)) (op (F.obj (unop X))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
rw :
  Eq.{v_2 + 1} (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
    (𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X))
    (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m h)) X))) ≫
      CategoryStruct.comp (Y := op ((F ⋙ shiftFunctor D m).obj (unop X)))
        (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F m)) (unop X)))
        (NatTrans.app (Iso.inv (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
          NatTrans.app (Iso.hom (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F m)) (unop X)) ≫
              Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m h)) X)))))
⊢ Eq (α := (F.op ⋙ shiftFunctor Dᵒᵖ n).obj X ⟶ (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
    (NatTrans.app (Iso.inv (commShiftIso F.op n)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F m)) (unop X)) ≫
        Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m h)) X))))

Tactic:
rw [← cancel_epi ((F.op.commShiftIso n).hom.app X), Iso.hom_inv_id_app,
    op_commShiftIso_hom_app _ X n m h, assoc, assoc]

Premises used: CategoryTheory.Functor.op, CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.op_commShiftIso_hom_app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ Eq.{v_2 + 1} (α := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X ⟶ (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
    (𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X))
    (Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso C n m h)) X))) ≫
      CategoryStruct.comp (Y := op ((F ⋙ shiftFunctor D m).obj (unop X)))
        (Quiver.Hom.op (NatTrans.app (Iso.inv (commShiftIso F m)) (unop X)))
        (NatTrans.app (Iso.inv (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
          NatTrans.app (Iso.hom (shiftFunctorOpIso D n m h)) (op (F.obj (unop X))) ≫
            Quiver.Hom.op (NatTrans.app (Iso.hom (commShiftIso F m)) (unop X)) ≫
              Quiver.Hom.op (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n m h)) X)))))

Tactic:
simp [← op_comp, ← F.map_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X Y : C
f : X ⟶ Y
n : ℤ
⊢ Eq (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj Y)) ⟶
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj X)))
    (map (shiftFunctor Dᵒᵖ n) (F.map f).op)
    (CategoryStruct.comp (Y := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj (op Y))
      (NatTrans.app (Iso.inv (commShiftIso F.op n)) (op Y))
      (CategoryStruct.comp (Y := op (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) (op X)))))
        (Quiver.Hom.op (F.map (Quiver.Hom.unop (map (shiftFunctor Cᵒᵖ n) f.op))))
        (NatTrans.app (Iso.hom (commShiftIso F.op n)) (op X))))

Tactic:
(NatIso.naturality_1 (F.op.commShiftIso n) f.op).symm

Premises used: CategoryTheory.Functor.op, CategoryTheory.NatIso.naturality_1, Quiver.Hom.op, Quiver.Hom.unop, Eq.symm, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X Y : Cᵒᵖ
f : X ⟶ Y
n : ℤ
⊢ Eq (α :=
    F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) Y)) ⟶
      F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
    (F.map (Quiver.Hom.unop (map (shiftFunctor Cᵒᵖ n) f)))
    (CategoryStruct.comp (Y := unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj Y))
      (Quiver.Hom.unop (NatTrans.app (Iso.inv (commShiftIso F.op n)) Y))
      (CategoryStruct.comp (Y := unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X)))))
        (Quiver.Hom.unop (map (shiftFunctor Dᵒᵖ n) (F.map f.unop).op) :
          unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop Y)))) ⟶
            unop (obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n) (op (F.obj (unop X)))))
        (Quiver.Hom.unop (NatTrans.app (Iso.hom (commShiftIso F.op n)) X) :
          unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X) ⟶ unop ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X))))

Tactic:
simp [shift_map_op]

Premises used: CategoryTheory.Functor.shift_map_op
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
e_a :
  Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
        map (shiftFunctor D n)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
          (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))) ⟶
        F.obj (unop X))
⊢ Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C n) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))) ⟶
      F.obj (unop X))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X))))
    (CategoryStruct.comp (Y :=
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X))))
      (NatTrans.app (Iso.hom (commShiftIso F n)) (unop (obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ n) X)))
      (map (shiftFunctor D n) (F.map (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso C n (-n) ⋯)) X))) ≫
        CategoryStruct.comp (Y :=
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
            (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))))
          (map (shiftFunctor D n) (NatTrans.app (Iso.hom (commShiftIso F (-n))) (unop X)))
          (map (shiftFunctor D n)
              (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
            map (shiftFunctor D n)
                (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
              NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))))

Tactic:
congr 3
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
e_a :
  Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
    (map (shiftFunctor D n)
        (Quiver.Hom.unop (𝟙 (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X)))))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n)
          (Quiver.Hom.unop (NatTrans.app (Iso.hom (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
        map (shiftFunctor D n)
            (Quiver.Hom.unop (NatTrans.app (Iso.inv (shiftFunctorOpIso D n (-n) ⋯)) (op (F.obj (unop X))))) ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
          (unop (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X))))) ⟶
        F.obj (unop X))

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

Premises used: CategoryTheory.unop_comp, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
e_a :
  Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n) (𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
        F.obj (unop X))
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) ((F ⋙ shiftFunctor D (-n)).obj (unop X)) ⟶
      obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
    (map (shiftFunctor D n)
        (Quiver.Hom.unop (𝟙 (obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D (-n))) (op (F.obj (unop X)))))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
e_a :
  NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) =
    𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X))
e_a₁ e_a₂ :
  Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)))
⊢ Eq.{v_2 + 1} (α :=
    obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
      F.obj (unop X))
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n) ⋙ shiftFunctor D n) (F.obj (unop X)) ⟶
        obj.{v_2, v_2, u_2, u_2} (𝟭 D) (F.obj (unop X)))
    (map (shiftFunctor D n) (𝟙 (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X)))) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId D (-n) n ⋯)) (F.obj (unop X)) :
      obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (-n)) (F.obj (unop X))) ⟶
        F.obj (unop X))

Tactic:
rw [map_id, id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq (α := F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)) ⟶ F.obj (unop (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)))
    (F.map (Quiver.Hom.unop (𝟙 (obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X))))
    (CategoryStruct.comp (Y :=
      unop
        (obj.{v_2, v_2, u_2, u_2}
          (Equivalence.functor (opShiftFunctorEquivalence D n) ⋙ Equivalence.inverse (opShiftFunctorEquivalence D n))
          (op (F.obj (unop X)))))
      (Quiver.Hom.unop
        (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))))
      (CategoryStruct.comp (Y := obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)))
        (map (shiftFunctor D n)
            (Quiver.Hom.unop
              (CategoryStruct.comp (Y := (shiftFunctor Cᵒᵖ n ⋙ F.op).obj X)
                (NatTrans.app (Iso.inv (commShiftIso F.op n)) X) (NatTrans.app (Iso.hom (commShiftIso F.op n)) X))) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n)
              (unop
                (obj.{v_2, v_2, u_2, u_2} (Equivalence.functor (opShiftFunctorEquivalence D n))
                  (op (F.obj (unop X))))) ⟶
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (unop ((F.op ⋙ shiftFunctor Dᵒᵖ n).obj X)))
        (Quiver.Hom.unop
            (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
          unop
              (obj.{v_2, v_2, u_2, u_2}
                (Equivalence.functor (opShiftFunctorEquivalence D n) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence D n))
                (op (F.obj (unop X)))) ⟶
            unop (obj.{v_2, v_2, u_2, u_2} (𝟭 Dᵒᵖ) (op (F.obj (unop X)))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ Eq.{v_2 + 1} (α := F.obj (unop X) ⟶ F.obj (unop X)) (𝟙 (F.obj (unop X)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y :=
        obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
          (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))))
        (NatTrans.app (Iso.inv (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X))) :
          obj.{v_2, v_2, u_2, u_2} (𝟭 Dᵒᵖ) (op (F.obj (unop X))) ⟶
            obj.{v_2, v_2, u_2, u_2} (Functor.op (shiftFunctor D n) ⋙ shiftFunctor Dᵒᵖ n) (op (F.obj (unop X))))
        (CategoryStruct.comp (Y :=
            obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
              (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))))
            (map (shiftFunctor Dᵒᵖ n) (Quiver.Hom.op (𝟙 ((F ⋙ shiftFunctor D n).obj (unop X)))))
            (NatTrans.app (Iso.hom (Equivalence.counitIso (opShiftFunctorEquivalence D n))) (op (F.obj (unop X)))) :
          obj.{v_2, v_2, u_2, u_2} (shiftFunctor Dᵒᵖ n)
              (op (obj.{v_2, v_2, u_2, u_2} (shiftFunctor D n) (F.obj (unop X)))) ⟶
            op (F.obj (unop X)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₁ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))) ≫
      Iso.hom
        (Iso.refl (Triangle.obj₂ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))))) =
    Iso.hom
        (Iso.refl (Triangle.obj₁ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))))) ≫
      Triangle.mor₁ (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₂ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))) ≫
      Iso.hom
        (Iso.refl (Triangle.obj₃ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))))) =
    Iso.hom
        (Iso.refl (Triangle.obj₂ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))))) ≫
      Triangle.mor₂ (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
T : Triangle.{v_1, u_1} C
⊢ Triangle.mor₃ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))) ≫
      map (shiftFunctor Dᵒᵖ (A := ℤ) 1)
        (Iso.hom
          (Iso.refl (Triangle.obj₁ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T)))))) =
    Iso.hom
        (Iso.refl (Triangle.obj₃ (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle T))))) ≫
      Triangle.mor₃ (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op T)))

Tactic:
simp [shift_map_op, map_opShiftFunctorEquivalence_counitIso_inv_app_unop]

Premises used: CategoryTheory.Functor.shift_map_op, CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_inv_app_unop
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : HasShift.{v_2, u_2, 0} D ℤ
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.CommShift ℤ
inst_5 : HasZeroObject.{v_1, u_1} C
inst_6 : Preadditive.{v_1, u_1} C
inst_7 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_8 : Pretriangulated.{v_1, u_1} C
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
X Y : (Triangle.{v_1, u_1} C)ᵒᵖ
f : X ⟶ Y
h₁ :
  Eq.{v_2 + 1} (α := op (F.obj (unop X).obj₃) ⟶ op (F.obj (unop Y).obj₃))
    ((F.map f.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y).obj₃))) (𝟙 (op (F.obj (unop X).obj₃)) ≫ (F.map f.unop.hom₃).op)
⊢ Eq (α :=
    Triangle.obj₁ (obj (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) X) ⟶
      Triangle.obj₁ (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) Y))
    (TriangleMorphism.hom₁
      (map (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) f ≫
        Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            Y)))
    (TriangleMorphism.hom₁
      (Iso.hom
          ((fun (T : (Triangle.{v_1, u_1} C)ᵒᵖ) ↦
              (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop T) :
                Iso (C := Triangle.{v_2, u_2} Dᵒᵖ)
                  (obj (Equivalence.functor (triangleOpEquivalence D)) (op (obj F.mapTriangle (unop T))))
                  (obj F.op.mapTriangle (obj (Equivalence.functor (triangleOpEquivalence C)) (op (unop T))))))
            X) ≫
        map (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) f))

Tactic:
dsimp