-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Functor (goal)
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
⊢ Eq (α :=
    Quiver.Hom (V := Triangle.{v_2, u_2} Dᵒᵖ)
      (obj (Functor.op F.mapTriangle ⋙ Equivalence.functor (triangleOpEquivalence D)) X)
      (obj (Equivalence.functor (triangleOpEquivalence C) ⋙ F.op.mapTriangle) Y))
    (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))
    (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)
have h₁ : 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: ext