-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
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)
⊢ Eq (α := (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X))
    ((functorEnrichedHomCoyonedaObjEquiv M F G X :
          (a : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)) →
            (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op 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 (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).map f.op) :
          (a : (fun (X : Type (max (max u₁ v₁) v₃)) ↦ X) ((presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op Y))) →
            (fun (X : Type (max (max u₁ v₁) v₃)) ↦ X) ((presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)))
        ((functorEnrichedHomCoyonedaObjEquiv M F G Y :
            (a : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op Y)) →
              (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op Y))
          y) :
      (fun (X : Type (max (max u₁ v₁) v₃)) ↦ X)
        ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).obj (op X)))
have dsimp : 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: dsimp