-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic (goal)
Goal:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} J₁
inst_1 : Category.{v₂, u₂} J₂
inst_2 : Category.{v₃, u₃} C
inst_3 : MonoidalCategory.{v₃, u₃} C
inst_4 : BraidedCategory.{v₃, u₃} C
X Y : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C
x : X ⟶ Y
⊢ Eq (α :=
    obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) X ⟶
      obj (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙ externalProductBifunctor J₂ J₁ C)
        Y)
    (map (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x ≫
      Iso.hom
        ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
            (NatIso.ofComponents
                (fun (x_1 : J₂ × J₁) ↦
                  β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2))
                ⋯ :
              obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x ≅
                obj
                  (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                    externalProductBifunctor J₂ J₁ C)
                  x))
          Y))
    (Iso.hom
        ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
            (NatIso.ofComponents
                (fun (x_1 : J₂ × J₁) ↦
                  β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_1).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_1).2))
                ⋯ :
              obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x ≅
                obj
                  (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                    externalProductBifunctor J₂ J₁ C)
                  x))
          X) ≫
      map (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙ externalProductBifunctor J₂ J₁ C)
        x)
have w : ∀ (x_1 : J₂ × J₁),
  Eq (α :=
    (obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) X).obj x_1 ⟶
      (obj
            (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
              externalProductBifunctor J₂ J₁ C)
            Y).obj
        x_1)
    (NatTrans.app
      (map (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁)) x ≫
        Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₂ × J₁) ↦
                    β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_2).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_2).2))
                  sorry :
                obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁))
                    x ≅
                  obj
                    (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                      externalProductBifunctor J₂ J₁ C)
                    x))
            Y))
      x_1)
    (NatTrans.app
      (Iso.hom
          ((fun (x : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₂, v₃, u₂, u₃} J₂ C) ↦
              (NatIso.ofComponents
                  (fun (x_2 : J₂ × J₁) ↦
                    β_ (x.1.obj (obj (Prod.swap J₂ J₁) x_2).1) (x.2.obj (obj (Prod.swap J₂ J₁) x_2).2))
                  sorry :
                obj (externalProductBifunctor J₁ J₂ C ⋙ obj (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C) (Prod.swap J₂ J₁))
                    x ≅
                  obj
                    (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙
                      externalProductBifunctor J₂ J₁ C)
                    x))
            X) ≫
        map
          (Prod.swap (Functor.{v₁, v₃, u₁, u₃} J₁ C) (Functor.{v₂, v₃, u₂, u₃} J₂ C) ⋙ externalProductBifunctor J₂ J₁ C)
          x)
      x_1)
Tactic: ext