awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
      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)
          (M.unmop ◁ Quiver.Hom.unmop MonObj.one :
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
              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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
        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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
        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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ M.unmop)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop)
        (M.unmop ◁ Quiver.Hom.unmop MonObj.one :
          tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
            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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ M.unmop)
    (Iso.hom (ρ_ M.unmop) : tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶ 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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
      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)
          (M.unmop ◁ Quiver.Hom.unmop MonObj.one :
            tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
              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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
        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) M.unmop (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⟶
        Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) M.unmop)

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
⊢ 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:
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.functor (mopEquiv C)) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.one ≫ f.unmop))
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) MonObj.one)
⊢ Eq (α := tensorUnit.{v_1, u_1} C (𝒞 := inst) ⟶ N.unmop) (MonObj.one ≫ f.unmop) MonObj.one

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
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.functor (mopEquiv C)) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.one ≫ f.unmop))
    (CategoryTheory.Functor.map (Equivalence.functor (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.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.mul ≫ f.unmop))
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) ((f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul))
⊢ Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop ⟶ N.unmop) (MonObj.mul ≫ f.unmop)
    ((f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul)

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
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.functor (mopEquiv C))
        (tensorObj.{v_1, u_1} (𝒞 := inst) M.unmop M.unmop) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (Equivalence.functor (mopEquiv C)) N.unmop)
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) (MonObj.mul ≫ f.unmop))
    (CategoryTheory.Functor.map (Equivalence.functor (mopEquiv C)) ((f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul))

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

Premises used: CategoryTheory.IsMonHom.mul_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
⊢ Function.Injective.{u₁ + 1, u₁ + 1} (α := C) mop

Tactic:
@mop.inj C

Premises used: CategoryTheory.MonoidalOpposite.mop.inj, Function.Injective
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
⊢ Function.Injective.{u₁ + 1, u₁ + 1} (α := Cᴹᵒᵖ) unmop

Tactic:
fun _ _ h => congrArg mop h

Premises used: CategoryTheory.MonoidalOpposite.mop, congrArg, Function.Injective
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
x y : C
⊢ { unmop := x : Cᴹᵒᵖ } = { unmop := y } ↔ x = y

Tactic:
mop_injective.eq_iff

Premises used: Function.Injective.eq_iff, CategoryTheory.MonoidalOpposite.mop_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
x y : Cᴹᵒᵖ
⊢ x.unmop = y.unmop ↔ x = y

Tactic:
unmop_injective.eq_iff

Premises used: Function.Injective.eq_iff, CategoryTheory.MonoidalOpposite.unmop_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
X : Cᴹᵒᵖ
⊢ { unmop := X.unmop : Cᴹᵒᵖ } = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
X : C
⊢ { unmop := X : Cᴹᵒᵖ }.unmop = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
⊢ Function.Injective.{v₁ + 1, v₁ + 1} (α := X ⟶ Y) mop

Tactic:
fun _ _ H => congr_arg Quiver.Hom.unmop H

Premises used: Quiver.Hom.unmop, congr_arg, Function.Injective
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᴹᵒᵖ
⊢ Function.Injective.{v₁ + 1, v₁ + 1} (α := X ⟶ Y) unmop

Tactic:
fun _ _ H => congr_arg Quiver.Hom.mop H

Premises used: congr_arg, Function.Injective, Quiver.Hom.mop
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ f.mop.unmop = f

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᴹᵒᵖ
f : X ⟶ Y
⊢ f.unmop.mop = f

Tactic:
rfl

Premises used: Quiver.Hom.unmop, Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).mop = f.mop ≫ g.mop

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := { unmop := X : Cᴹᵒᵖ } ⟶ { unmop := X }) (Quiver.Hom.mop (𝟙 X)) (𝟙 { unmop := X })

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : Cᴹᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).unmop = f.unmop ≫ g.unmop

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α := X.unmop ⟶ X.unmop) (Quiver.Hom.unmop (𝟙 X)) (𝟙 X.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := { unmop := X : Cᴹᵒᵖ }.unmop ⟶ { unmop := X }.unmop) (Quiver.Hom.unmop (𝟙 { unmop := X })) (𝟙 X)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α := { unmop := X.unmop : Cᴹᵒᵖ } ⟶ { unmop := X.unmop }) (Quiver.Hom.mop (𝟙 X.unmop)) (𝟙 X)

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
x y : Cᴹᵒᵖ
f g : x ⟶ y
h : f.unmop = g.unmop
⊢ f = g

Tactic:
Quiver.Hom.unmop_inj h

Premises used: Quiver.Hom.unmop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.mop

Tactic:
(mopFunctor C).map_isIso f

Premises used: CategoryTheory.mopFunctor, CategoryTheory.Functor.map_isIso, Quiver.Hom.mop
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᴹᵒᵖ
f : X ⟶ Y
inst_1 : IsIso f
⊢ IsIso f.unmop

Tactic:
(unmopFunctor C).map_isIso f

Premises used: CategoryTheory.unmopFunctor, Quiver.Hom.unmop, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Cᵒᵖ
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : Y₁ ⟶ Z₁
x_3 : Y₂ ⟶ Z₂
⊢ Eq (α :=
    unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Z₁) (unop Z₂))) ⟶
      unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X₁) (unop X₂))))
    (Quiver.Hom.unop (Quiver.Hom.op (x.unop ⊗ₘ x_1.unop) ≫ Quiver.Hom.op (x_2.unop ⊗ₘ x_3.unop)))
    (Quiver.Hom.unop (Quiver.Hom.op ((x ≫ x_2).unop ⊗ₘ (x_1 ≫ x_3).unop)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Cᵒᵖ
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
h : X₃ ⟶ Y₃
⊢ Eq (α :=
    unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y₁) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y₂) (unop Y₃)))))) ⟶
      unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X₁) (unop X₂)))) (unop X₃))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (f.unop ⊗ₘ g.unop)) ⊗ₘ h.unop) ≫
        Iso.hom (Iso.op (Iso.symm (α_ (unop Y₁) (unop Y₂) (unop Y₃))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (α_ (unop X₁) (unop X₂) (unop X₃)))) ≫
        Quiver.Hom.op (f.unop ⊗ₘ Quiver.Hom.unop (Quiver.Hom.op (g.unop ⊗ₘ h.unop)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := unop Y ⟶ unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (unop X))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ◁ f.unop) ≫
        Iso.hom (Iso.op (Iso.symm (λ_ (unop Y))))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λ_ (unop X)))) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := unop Y ⟶ unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (f.unop ▷ unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.hom (Iso.op (Iso.symm (ρ_ (unop Y))))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρ_ (unop X)))) ≫ f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X Y Z : Cᵒᵖ
dsimp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (unop W)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y)) (unop Z))
    ((unop W ◁ Iso.inv (α_ (unop X) (unop Y) (unop Z)) ≫
        Iso.inv (α_ (unop W) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)) (unop Z))) ≫
      Iso.inv (α_ (unop W) (unop X) (unop Y)) ▷ unop Z)
    (Iso.inv (α_ (unop W) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y) (unop Z)))
⊢ Eq (α :=
    unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W)
            (unop
              (op
                (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X)
                  (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))))))))) ⟶
      unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (unop
              (op
                (tensorObj.{v₁, u₁} (𝒞 := inst) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X))))
                  (unop Y))))
            (unop Z))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (α_ (unop W) (unop X) (unop Y))))) ▷ unop Z) ≫
        Iso.hom
            (Iso.op (Iso.symm (α_ (unop W) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)))) (unop Z)))) ≫
          Quiver.Hom.op (unop W ◁ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (α_ (unop X) (unop Y) (unop Z))))))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (α_ (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)))) (unop Y) (unop Z)))) ≫
        Iso.hom
          (Iso.op (Iso.symm (α_ (unop W) (unop X) (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z)))))))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
W X Y Z : Cᵒᵖ
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (unop W)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y)) (unop Z))
    ((unop W ◁ Iso.inv (α_ (unop X) (unop Y) (unop Z)) ≫
        Iso.inv (α_ (unop W) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)) (unop Z))) ≫
      Iso.inv (α_ (unop W) (unop X) (unop Y)) ▷ unop Z)
    (Iso.inv (α_ (unop W) (unop X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop Y) (unop Z))) ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop X)) (unop Y) (unop Z)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (unop Y))
    (unop X ◁ Iso.inv (λ_ (unop Y)) ≫ Iso.inv (α_ (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop Y)))
    (Iso.inv (ρ_ (unop X)) ▷ unop Y)
⊢ Eq.{v₁ + 1} (α :=
    unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y))) ⟶
      unop
        (op
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (unop (op (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))))
            (unop Y))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (α_ (unop X) (unop (op (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (unop Y)))) ≫
        Quiver.Hom.op (unop X ◁ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λ_ (unop Y))))))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρ_ (unop X))))) ▷ unop Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (unop Y))
    (unop X ◁ Iso.inv (λ_ (unop Y)) ≫ Iso.inv (α_ (unop X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop Y)))
    (Iso.inv (ρ_ (unop X)) ▷ unop Y)

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
⊢ op (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) = tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op X) (op Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
⊢ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Y) = tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ op (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
⊢ unop (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) = tensorUnit.{v₁, u₁} C (𝒞 := inst)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂))
    (Quiver.Hom.op (f ⊗ₘ g)) (f.op ⊗ₘ g.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Cᵒᵖ
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) Y₁ Y₂) ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X₁ X₂))
    (Quiver.Hom.unop (f ⊗ₘ g)) (f.unop ⊗ₘ g.unop)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Quiver.Hom.op (X ◁ f))
    (op X ◁ f.op)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : Y ⟶ Z
⊢ Eq (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Z) ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Y))
    (Quiver.Hom.unop (X ◁ f)) (unop X ◁ f.unop)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)) (Quiver.Hom.op (f ▷ Z))
    (f.op ▷ op Z)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : Cᵒᵖ
⊢ Eq (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) Y Z) ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Z))
    (Quiver.Hom.unop (f ▷ Z)) (f.unop ▷ unop Z)

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl