awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
g : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X_1 g ⟶ tensorObj.{v, u} (𝒞 := inst) g Y_1)
    (f ▷ g ≫ Iso.hom (coprod.braiding Y_1 g))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) g X_1)
      (Iso.hom (coprod.braiding X_1 g) : tensorObj.{v, u} (𝒞 := inst) X_1 g ⟶ tensorObj.{v, u} (𝒞 := inst) g X_1)
      (g ◁ f : tensorObj.{v, u} (𝒞 := inst) g X_1 ⟶ tensorObj.{v, u} (𝒞 := inst) g Y_1))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
dsimp :
  Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X Y) Z ⟶ coprod.{v, u} Y (coprod.{v, u} Z X))
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Y Z))
      (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y Z) X) (coprod.desc coprod.inr coprod.inl)
        (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y X) Z)
      (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Z))
      (CategoryStruct.comp (Y := coprod.{v, u} Y (coprod.{v, u} X Z))
        (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
        (coprod.map (𝟙 Y) (coprod.desc coprod.inr coprod.inl))))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
    (Iso.hom (α_ X Y Z) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
        (Iso.hom (coprod.braiding X (tensorObj.{v, u} (𝒞 := inst) Y Z)) :
          tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
            tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
        (Iso.hom (α_ Y Z X) :
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X ⟶
            tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X)))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z)
      (Iso.hom (coprod.braiding X Y) ▷ Z :
        tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z)
      (Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (coprod.braiding X Z) :
        tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y X) Z ⟶
          tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X)))

Tactic:
dsimp [monoidalOfHasFiniteCoproducts.associator_hom]

Premises used: CategoryTheory.monoidalOfHasFiniteCoproducts.associator_hom
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α := coprod.{v, u} (coprod.{v, u} X Y) Z ⟶ coprod.{v, u} Y (coprod.{v, u} Z X))
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Y Z))
      (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y Z) X) (coprod.desc coprod.inr coprod.inl)
        (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))))
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} Y X) Z)
      (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Z))
      (CategoryStruct.comp (Y := coprod.{v, u} Y (coprod.{v, u} X Z))
        (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))
        (coprod.map (𝟙 Y) (coprod.desc coprod.inr coprod.inl))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
dsimp :
  Eq.{v + 1} (α := coprod.{v, u} X (coprod.{v, u} Y Z) ⟶ coprod.{v, u} (coprod.{v, u} Z X) Y)
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Y) Z)
      (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
      (CategoryStruct.comp (Y := coprod.{v, u} Z (coprod.{v, u} X Y)) (coprod.desc coprod.inr coprod.inl)
        (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))))
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Z Y))
      (coprod.map (𝟙 X) (coprod.desc coprod.inr coprod.inl))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Z) Y)
        (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
        (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Y))))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y)
    (Iso.inv (α_ X Y Z) ≫
      CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y))
        (Iso.hom (coprod.braiding (tensorObj.{v, u} (𝒞 := inst) X Y) Z) :
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
            tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y))
        (Iso.inv (α_ Z X Y) :
          tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y) ⟶
            tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y))
      (X ◁ Iso.hom (coprod.braiding Y Z) :
        tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
          tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y))
      (Iso.inv (α_ X Z Y) ≫ Iso.hom (coprod.braiding X Z) ▷ Y :
        tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Z Y) ⟶
          tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))

Tactic:
dsimp [monoidalOfHasFiniteCoproducts.associator_inv]

Premises used: CategoryTheory.monoidalOfHasFiniteCoproducts.associator_inv
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α := coprod.{v, u} X (coprod.{v, u} Y Z) ⟶ coprod.{v, u} (coprod.{v, u} Z X) Y)
    (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Y) Z)
      (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
      (CategoryStruct.comp (Y := coprod.{v, u} Z (coprod.{v, u} X Y)) (coprod.desc coprod.inr coprod.inl)
        (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))))
    (CategoryStruct.comp (Y := coprod.{v, u} X (coprod.{v, u} Z Y))
      (coprod.map (𝟙 X) (coprod.desc coprod.inr coprod.inl))
      (CategoryStruct.comp (Y := coprod.{v, u} (coprod.{v, u} X Z) Y)
        (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))
        (coprod.map (coprod.desc coprod.inr coprod.inl) (𝟙 Y))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) Y X)
        (Iso.hom (coprod.braiding X Y) : tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) Y X)
        (Iso.hom (coprod.braiding Y X) : tensorObj.{v, u} (𝒞 := inst) Y X ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) :
      tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) : tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
simp
-- 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.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
          (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Quiver.Hom.mop MonObj.one ▷ { unmop := M } ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (λ_ { unmop := M })))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
        { unmop := M : Cᴹᵒᵖ } ⟶
      { unmop := M })
    (Quiver.Hom.mop MonObj.one ▷ { unmop := M } ≫ Quiver.Hom.mop MonObj.mul) (Iso.hom (λ_ { unmop := M }))

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
          (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Quiver.Hom.mop MonObj.one ▷ { unmop := M } ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (λ_ { unmop := M })))

Tactic:
simp
-- 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.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ }
          (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      ({ unmop := M } ◁ Quiver.Hom.mop MonObj.one ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (ρ_ { unmop := M })))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ }
        (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ⟶
      { unmop := M })
    ({ unmop := M } ◁ Quiver.Hom.mop MonObj.one ≫ Quiver.Hom.mop MonObj.mul) (Iso.hom (ρ_ { unmop := M }))

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ }
          (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      ({ unmop := M } ◁ Quiver.Hom.mop MonObj.one ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (Iso.hom (ρ_ { unmop := M })))

Tactic:
simp
-- 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.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
          (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ })
          { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Quiver.Hom.mop MonObj.mul ▷ { unmop := M : Cᴹᵒᵖ } ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Iso.hom (α_ { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ≫
        { unmop := M : Cᴹᵒᵖ } ◁ Quiver.Hom.mop MonObj.mul ≫ Quiver.Hom.mop MonObj.mul))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ })
        { unmop := M : Cᴹᵒᵖ } ⟶
      { unmop := M })
    (Quiver.Hom.mop MonObj.mul ▷ { unmop := M : Cᴹᵒᵖ } ≫ Quiver.Hom.mop MonObj.mul)
    (Iso.hom (α_ { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ≫
      { unmop := M : Cᴹᵒᵖ } ◁ Quiver.Hom.mop MonObj.mul ≫ Quiver.Hom.mop MonObj.mul)

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
          (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ })
          { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := M : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Quiver.Hom.mop MonObj.mul ▷ { unmop := M : Cᴹᵒᵖ } ≫ Quiver.Hom.mop MonObj.mul))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C))
      (Iso.hom (α_ { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ≫
        { unmop := M : Cᴹᵒᵖ } ◁ Quiver.Hom.mop MonObj.mul ≫ Quiver.Hom.mop MonObj.mul))

Tactic:
simp
-- 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
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
apply :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.one ≫ f.mop))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) MonObj.one)
⊢ Eq (α := tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory) ⟶ { unmop := N : Cᴹᵒᵖ }) (MonObj.one ≫ f.mop)
    MonObj.one

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorUnit.{v_1, u_1} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.one ≫ f.mop))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) MonObj.one)

Tactic:
simpa [-IsMonHom.one_hom] using IsMonHom.one_hom f

Premises used: CategoryTheory.IsMonHom.one_hom
-- 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
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
apply :
  Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.mul ≫ f.mop))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) ((f.mop ⊗ₘ f.mop) ≫ MonObj.mul))
⊢ Eq (α :=
    tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ } ⟶ { unmop := N })
    (MonObj.mul ≫ f.mop) ((f.mop ⊗ₘ f.mop) ≫ MonObj.mul)

Tactic:
apply mopEquiv C |>.fullyFaithfulInverse.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
N : C
inst_3 : MonObj N
f : M ⟶ N
inst_4 : IsMonHom f
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := M : Cᴹᵒᵖ } { unmop := M : Cᴹᵒᵖ }) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.inverse (mopEquiv C)) { unmop := N : Cᴹᵒᵖ })
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) (MonObj.mul ≫ f.mop))
    (CategoryTheory.Functor.map (Equivalence.inverse (mopEquiv C)) ((f.mop ⊗ₘ f.mop) ≫ MonObj.mul))

Tactic:
simpa [-IsMonHom.mul_hom] using IsMonHom.mul_hom f

Premises used: CategoryTheory.IsMonHom.mul_hom
-- 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) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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.one ▷ M.unmop :
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (Quiver.Hom.unmop MonObj.one ▷ M.unmop :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)
    (Iso.hom (λ_ M.unmop) : tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop ⟶ M.unmop)

Tactic:
apply mopEquiv C |>.fullyFaithfulFunctor.map_injective

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.MonoidalOpposite.mopEquiv
-- 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
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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.one ▷ M.unmop :
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) 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)) :
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C))
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) M.unmop) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)

Tactic:
simp