-- Mathlib/CategoryTheory/Sites/Monoidal.lean
lemma functorEnrichedHomCoyonedaObjEquiv_naturality
    {M : A} {F G : Cᵒᵖ ⥤ A} {X Y : C} (f : X ⟶ Y)
    [HasFunctorEnrichedHom A F G]
    (y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)) :
    functorEnrichedHomCoyonedaObjEquiv M F G X
      (y ≫ precompEnrichedHom' _ (Under.map f.op) (Iso.refl _) (Iso.refl _)) =
    (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).map f.op
      (functorEnrichedHomCoyonedaObjEquiv M F G Y y)

Proof state:
C : Type u'
inst✝⁴ : Category.{v', u'} C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
⊢ (functorEnrichedHomCoyonedaObjEquiv M F G X)
      (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))) =
    (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).map f.op ((functorEnrichedHomCoyonedaObjEquiv M F G Y) y)

Tactic:
ext ⟨j⟩

Result:
case w.h.op
C : Type u'
inst✝⁴ : Category.{v', u'} C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
j : Over X
⊢ ((functorEnrichedHomCoyonedaObjEquiv M F G X)
          (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)))).app
      (op j) =
    ((presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).map f.op ((functorEnrichedHomCoyonedaObjEquiv M F G Y) y)).app
      (op j)

Proof state:
case w.h.op
C : Type u'
inst✝⁴ : Category.{v', u'} C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
j : Over X
⊢ ((functorEnrichedHomCoyonedaObjEquiv M F G X)
          (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)))).app
      (op j) =
    ((presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).map f.op ((functorEnrichedHomCoyonedaObjEquiv M F G Y) y)).app
      (op j)

Tactic:
simp [functorEnrichedHomCoyonedaObjEquiv, presheafHom]

Result:
case w.h.op
C : Type u'
inst✝⁴ : Category.{v', u'} C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
j : Over X
⊢ MonoidalClosed.uncurry
      (y ≫
        enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) ((Under.map f.op).obj (Under.mk j.hom.op))) =
    MonoidalClosed.uncurry
      (y ≫ enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) (Under.mk (f.op ≫ j.hom.op)))

Proof state:
case w.h.op
C : Type u'
inst✝⁴ : Category.{v', u'} C
A : Type u
inst✝³ : Category.{v, u} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
X Y : C
f : X ⟶ Y
inst✝ : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)
j : Over X
⊢ MonoidalClosed.uncurry
      (y ≫
        enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) ((Under.map f.op).obj (Under.mk j.hom.op))) =
    MonoidalClosed.uncurry
      (y ≫ enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G) (Under.mk (f.op ≫ j.hom.op)))

Tactic:
rfl

Result:
no goals