-- Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon
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
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)
⊢ 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)

Tactic:
apply mopEquiv C |>.fullyFaithfulFunctor.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.MonoidalOpposite.mopEquiv