-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Opposite.Mon (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
M : Cᴹᵒᵖ
inst_2 : MonObj M
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop ⟶ M.unmop)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul ▷ M.unmop :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop ⟶ M.unmop)
    (Iso.hom (α_ M.unmop M.unmop M.unmop) ≫
        CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
          (M.unmop ◁ Quiver.Hom.unmop MonObj.mul :
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
          (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop ⟶ M.unmop)
have apply : Eq.{v_1 + 1} (α :=
  Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
      (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop) ⟶
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C))
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul ▷ M.unmop :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop ⟶
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
  (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C))
      (Iso.hom (α_ M.unmop M.unmop M.unmop) ≫
        CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
          (M.unmop ◁ Quiver.Hom.unmop MonObj.mul :
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
          (Quiver.Hom.unmop MonObj.mul : (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) M M).unmop ⟶ M.unmop)) :
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)
Tactic: apply mopEquiv C |>.fullyFaithfulFunctor.map_injective