-- Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
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
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))
                    ⋯ :
                  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))
                    ⋯ :
                  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)
⊢ 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)

Tactic:
ext