-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
T₁ T₂ : Triangle.{v_1, u_1} Cᵒᵖ
hT₁ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
    (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₁))
hT₂ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_2 _ inst_3 inst_4 _)
    (Opposite.unop (Functor.obj (Equivalence.inverse (triangleOpEquivalence C)) T₂))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : Opposite.unop T₂.obj₃ ⟶ Opposite.unop T₁.obj₃
hc₁ : T₂.mor₂.unop ≫ b.unop = c ≫ T₁.mor₂.unop
hc₂ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) T₂.mor₃.unop ≫ Functor.map (shiftFunctor C (A := ℤ) 1) c)
    (Quiver.Hom.unop (NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₂.obj₁) ≫
      a.unop ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
            (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))
          (Quiver.Hom.unop (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₁.obj₁) :
            Opposite.unop T₁.obj₁ ⟶
              Opposite.unop
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)))))
          (Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop :
            Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁)) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃)))
a₁ :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Quiver.Hom.unop (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a)) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop)
    (Quiver.Hom.unop
        (CategoryStruct.comp (Y :=
          Opposite.op
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
              (Opposite.unop
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                  (Opposite.op
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                      (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁))))))))
          (Quiver.Hom.op
              (Functor.map (shiftFunctor C (A := ℤ) 1)
                (Quiver.Hom.unop
                  (Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                    (a ≫ NatTrans.app (Iso.hom (Equivalence.unitIso (opShiftFunctorEquivalence C 1))) T₂.obj₁)))) :
            Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₁.obj₁))) ⟶
              Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                  (Opposite.unop
                    (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1)
                      (Opposite.op
                        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                          (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁))))))))
          (NatTrans.app (Iso.inv (Equivalence.unitIso (opShiftFunctorEquivalence C 1)))
              (Opposite.op
                (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                  (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)))) :
            Functor.obj.{v_1, v_1, u_1, u_1}
                (Equivalence.functor (opShiftFunctorEquivalence C 1) ⋙
                  Equivalence.inverse (opShiftFunctorEquivalence C 1))
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)))) ⟶
              Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ)
                (Opposite.op
                  (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
                    (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)))))) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) T₁.mor₃.unop)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1)
        (Opposite.unop (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 1) T₂.obj₁)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Opposite.unop T₁.obj₃))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Quiver.Hom.unop (T₁.mor₃ ≫ Functor.map (shiftFunctor Cᵒᵖ (A := ℤ) 1) a)))
    (Functor.map (shiftFunctor C (A := ℤ) 1) (Quiver.Hom.unop (c.op ≫ T₂.mor₃)))

Tactic:
rw [unop_comp, unop_comp, Functor.map_comp, Functor.map_comp,
    Quiver.Hom.unop_op, hc₂, ← unop_comp_assoc, ← unop_comp_assoc,
    ← opShiftFunctorEquivalence_unitIso_inv_naturality]

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp, CategoryTheory.unop_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality