-- 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
X Y : Functor.{v₁, v₃, u₁, u₃} J₁ C × Functor.{v₁, v₃, u₁, u₃} J₁ C
x : X ⟶ Y
w :
  ∀ (x_1 : J₁),
    Eq (α :=
      (obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) X).obj x_1 ⟶
        (obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) Y).obj x_1)
      (NatTrans.app
        (map (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag 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₁) ↦
                      Iso.refl
                        ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                          x_2))
                    ⋯ :
                  obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                    obj (tensor (Functor.{v₁, v₃, u₁, u₃} 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₁) ↦
                      Iso.refl
                        ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                          x_2))
                    ⋯ :
                  obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                    obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x))
              X) ≫
          map (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x)
        x_1)
⊢ Eq (α :=
    obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) X ⟶
      obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) Y)
    (map (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag 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₁) ↦
                  Iso.refl
                    ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                      x_1))
                ⋯ :
              obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                obj (tensor (Functor.{v₁, v₃, u₁, u₃} 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₁) ↦
                  Iso.refl
                    ((obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x).obj
                      x_1))
                ⋯ :
              obj (externalProductBifunctor J₁ J₁ C ⋙ obj (whiskeringLeft J₁ (J₁ × J₁) C) (diag J₁)) x ≅
                obj (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x))
          X) ≫
      map (tensor (Functor.{v₁, v₃, u₁, u₃} J₁ C)) x)

Tactic:
ext