-- 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
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₁) 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)
have 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))
                  sorry :
                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))
                  sorry :
                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)
Tactic: ext