-- Module: Mathlib.CategoryTheory.Sites.Monoidal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
X Y : C
f : X ⟶ Y
inst_4 : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op Y)
w :
  ∀ (j : Over.{v₁, u₁} X),
    Eq.{v₃ + 1} (α :=
      (Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).obj
          (op j) ⟶
        (Functor.op (Over.forget X) ⋙ G).obj (op j))
      (NatTrans.app
        ((functorEnrichedHomCoyonedaObjEquiv M F G X :
            (a : M ⟶ enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) →
              (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
          (y ≫
            precompEnrichedHom' A (Under.map f.op) (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ F))
              (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ G))))
        (op j))
      (NatTrans.app
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).map f.op) :
            (a : (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G) →
              (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
          ((functorEnrichedHomCoyonedaObjEquiv M F G Y :
              (a : M ⟶ enrichedHom A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)) →
                (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G)
            y))
        (op j))
⊢ Eq (α :=
    Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M) ⟶
      Functor.op (Over.forget X) ⋙ G)
    ((functorEnrichedHomCoyonedaObjEquiv M F G X :
          (a : M ⟶ enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        (y ≫
          precompEnrichedHom' A (Under.map f.op) (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ F))
            (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ G))) :
      Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M) ⟶
        Functor.op (Over.forget X) ⋙ G)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).map f.op) :
          (a : (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        ((functorEnrichedHomCoyonedaObjEquiv M F G Y :
            (a : M ⟶ enrichedHom A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)) →
              (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G)
          y) :
      Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M) ⟶
        Functor.op (Over.forget X) ⋙ G)

Tactic:
ext ⟨j⟩