awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : C
⊢ Eq.{v₁ + 1} (α :=
    op (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≅
      op (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
    (Iso.op (α_ X Y Z)) (Iso.symm (α_ (op X) (op Y) (op Z)))

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.Iso.op, CategoryTheory.Iso.symm, 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ᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) Y Z)) ≅
      unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Y) Z))
    (Iso.unop (α_ X Y Z)) (Iso.symm (α_ (unop X) (unop Y) (unop Z)))

Tactic:
rfl

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

Tactic:
rfl

Premises used: Quiver.Hom.op, 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ᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) Y Z)) ⟶
      unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Y) Z))
    (Quiver.Hom.unop (Iso.hom (α_ X Y Z))) (Iso.inv (α_ (unop X) (unop Y) (unop 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 Z : C
⊢ Eq.{v₁ + 1} (α :=
    op (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      op (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Quiver.Hom.op (Iso.inv (α_ X Y Z))) (Iso.hom (α_ (op X) (op Y) (op Z)))

Tactic:
rfl

Premises used: Quiver.Hom.op, 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ᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X Y) Z) ⟶
      unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) Y Z)))
    (Quiver.Hom.unop (Iso.inv (α_ X Y Z))) (Iso.hom (α_ (unop X) (unop Y) (unop 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 : C
⊢ Eq.{v₁ + 1} (α := op X ≅ op (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X)) (Iso.op (λ_ X))
    (Iso.symm (λ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.Iso.op, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop X ≅ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) X))
    (Iso.unop (λ_ X)) (Iso.symm (λ_ (unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.symm, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := op X ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X))
    (Quiver.Hom.op (Iso.hom (λ_ X))) (Iso.inv (λ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop X ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) X))
    (Quiver.Hom.unop (Iso.hom (λ_ X))) (Iso.inv (λ_ (unop X)))

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 : C
⊢ Eq.{v₁ + 1} (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ⟶ op X)
    (Quiver.Hom.op (Iso.inv (λ_ X))) (Iso.hom (λ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) X) ⟶ unop X)
    (Quiver.Hom.unop (Iso.inv (λ_ X))) (Iso.hom (λ_ (unop X)))

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 : C
⊢ Eq.{v₁ + 1} (α := op X ≅ op (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.op (ρ_ X))
    (Iso.symm (ρ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, CategoryTheory.Iso.op, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop X ≅ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite))))
    (Iso.unop (ρ_ X)) (Iso.symm (ρ_ (unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.unop, CategoryTheory.Iso.symm, rfl, CategoryTheory.Iso.unop
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := op X ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Quiver.Hom.op (Iso.hom (ρ_ X))) (Iso.inv (ρ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop X ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite))))
    (Quiver.Hom.unop (Iso.hom (ρ_ X))) (Iso.inv (ρ_ (unop X)))

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 : C
⊢ Eq.{v₁ + 1} (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶ op X)
    (Quiver.Hom.op (Iso.inv (ρ_ X))) (Iso.hom (ρ_ (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) X (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite))) ⟶ unop X)
    (Quiver.Hom.unop (Iso.inv (ρ_ X))) (Iso.hom (ρ_ (unop X)))

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
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op X) (op Z) ⟶
      tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op W) (op Y))
    (f.op ⊗ₘ g.op) (Quiver.Hom.op (f ⊗ₘ g))

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
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (unop X) (unop Z) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop W) (unop Y))
    (f.unop ⊗ₘ g.unop) (Quiver.Hom.unop (f ⊗ₘ g))

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₁ X₂ Y₂ Z₂ : Cᴹᵒᵖ
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
x_2 : Y₁ ⟶ Z₁
x_3 : Y₂ ⟶ Z₂
⊢ Eq (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X₂.unmop X₁.unmop : Cᴹᵒᵖ }.unmop ⟶
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Z₂.unmop Z₁.unmop }.unmop)
    (Quiver.Hom.unmop (Quiver.Hom.mop (x_1.unmop ⊗ₘ x.unmop) ≫ Quiver.Hom.mop (x_3.unmop ⊗ₘ x_2.unmop)))
    (Quiver.Hom.unmop (Quiver.Hom.mop ((x_1 ≫ x_3).unmop ⊗ₘ (x ≫ x_2).unmop)))

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 (α :=
    {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) X₃.unmop
              { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X₂.unmop X₁.unmop : Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y₃.unmop Y₂.unmop }.unmop
              Y₁.unmop }.unmop)
    (Quiver.Hom.unmop
      (Quiver.Hom.mop (h.unmop ⊗ₘ Quiver.Hom.unmop (Quiver.Hom.mop (g.unmop ⊗ₘ f.unmop))) ≫
        Iso.hom (Iso.mop (Iso.symm (α_ Y₃.unmop Y₂.unmop Y₁.unmop)))))
    (Quiver.Hom.unmop
      (Iso.hom (Iso.mop (Iso.symm (α_ X₃.unmop X₂.unmop X₁.unmop))) ≫
        Quiver.Hom.mop (Quiver.Hom.unmop (Quiver.Hom.mop (h.unmop ⊗ₘ g.unmop)) ⊗ₘ f.unmop)))

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 (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      Y.unmop)
    (Quiver.Hom.unmop
      (Quiver.Hom.mop (f.unmop ▷ { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop) ≫
        Iso.hom (Iso.mop (ρ_ Y.unmop))))
    (Quiver.Hom.unmop (Iso.hom (Iso.mop (ρ_ X.unmop)) ≫ 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
⊢ (Quiver.Hom.mop ({ unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop ◁ f.unmop) ≫
        Iso.hom (Iso.mop (λ_ Y.unmop))).unmop =
    Quiver.Hom.unmop (Iso.hom (Iso.mop (λ_ X.unmop)) ≫ 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) Z.unmop
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop) W.unmop)
    (Z.unmop ◁ Iso.inv (α_ Y.unmop X.unmop W.unmop) ≫
      Iso.inv (α_ Z.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop) W.unmop) ≫
        Iso.inv (α_ Z.unmop Y.unmop X.unmop) ▷ W.unmop)
    (Iso.inv (α_ Z.unmop Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop W.unmop))
⊢ Eq (α :=
    {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop
                      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop : Cᴹᵒᵖ }.unmop :
                  Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst)
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop }.unmop
                      X.unmop }.unmop
              W.unmop }.unmop)
    (Quiver.Hom.unmop
      (Quiver.Hom.mop (Z.unmop ◁ Quiver.Hom.unmop (Iso.hom (Iso.mop (Iso.symm (α_ Y.unmop X.unmop W.unmop))))) ≫
        Iso.hom
            (Iso.mop
              (Iso.symm
                (α_ Z.unmop { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop : Cᴹᵒᵖ }.unmop W.unmop))) ≫
          Quiver.Hom.mop (Quiver.Hom.unmop (Iso.hom (Iso.mop (Iso.symm (α_ Z.unmop Y.unmop X.unmop)))) ▷ W.unmop)))
    (Quiver.Hom.unmop
      (Iso.hom
          (Iso.mop
            (Iso.symm (α_ Z.unmop Y.unmop { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop : Cᴹᵒᵖ }.unmop))) ≫
        Iso.hom
          (Iso.mop (Iso.symm (α_ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop }.unmop X.unmop W.unmop)))))

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) Z.unmop
        (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop) W.unmop)
    (Z.unmop ◁ Iso.inv (α_ Y.unmop X.unmop W.unmop) ≫
      Iso.inv (α_ Z.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop) W.unmop) ≫
        Iso.inv (α_ Z.unmop Y.unmop X.unmop) ▷ W.unmop)
    (Iso.inv (α_ Z.unmop Y.unmop (tensorObj.{v₁, u₁} (𝒞 := inst) X.unmop W.unmop)) ≫
      Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Z.unmop Y.unmop) X.unmop W.unmop))

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) Y.unmop
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop)
    (Iso.inv (α_ Y.unmop (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ≫ Iso.hom (ρ_ Y.unmop) ▷ X.unmop)
    (Y.unmop ◁ Iso.hom (λ_ X.unmop))
⊢ Eq.{v₁ + 1} (α :=
    {
          unmop :=
            tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop
              {
                  unmop :=
                    tensorObj.{v₁, u₁} (𝒞 := inst) { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop X.unmop :
                  Cᴹᵒᵖ }.unmop :
          Cᴹᵒᵖ }.unmop ⟶
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop }.unmop)
    (Quiver.Hom.unmop
      (Iso.hom (Iso.mop (Iso.symm (α_ Y.unmop { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ }.unmop X.unmop))) ≫
        Quiver.Hom.mop (Quiver.Hom.unmop (Iso.hom (Iso.mop (ρ_ Y.unmop))) ▷ X.unmop)))
    (Quiver.Hom.unmop (Quiver.Hom.mop (Y.unmop ◁ Quiver.Hom.unmop (Iso.hom (Iso.mop (λ_ X.unmop))))))

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) Y.unmop
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop)
    (Iso.inv (α_ Y.unmop (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X.unmop) ≫ Iso.hom (ρ_ Y.unmop) ▷ X.unmop)
    (Y.unmop ◁ Iso.hom (λ_ X.unmop))

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
⊢ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y : Cᴹᵒᵖ } =
    tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) { unmop := Y } { unmop := X }

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ᴹᵒᵖ
⊢ (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop = tensorObj.{v₁, u₁} (𝒞 := inst) Y.unmop X.unmop

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
⊢ { unmop := tensorUnit.{v₁, u₁} C (𝒞 := inst) : Cᴹᵒᵖ } = tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)

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
⊢ unmop (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)) = 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 (α := { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂ })
    (Quiver.Hom.mop (f ⊗ₘ g)) (g.mop ⊗ₘ f.mop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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 (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X₁ X₂).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y₁ Y₂).unmop)
    (Quiver.Hom.unmop (f ⊗ₘ g)) (g.unmop ⊗ₘ f.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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 (α := { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Z })
    (Quiver.Hom.mop (X ◁ f)) (f.mop ▷ { unmop := X })

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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 (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Z).unmop)
    (Quiver.Hom.unmop (X ◁ f)) (f.unmop ▷ X.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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 (α := { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Z : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y Z })
    (Quiver.Hom.mop (f ▷ Z)) ({ unmop := Z } ◁ f.mop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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 (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Z).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z).unmop)
    (Quiver.Hom.unmop (f ▷ Z)) (Z.unmop ◁ f.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z : Cᴹᵒᵖ } ≅
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) })
    (Iso.mop (α_ X Y Z)) (Iso.symm (α_ { unmop := Z } { unmop := Y } { unmop := X }))

Tactic:
rfl

Premises used: CategoryTheory.Iso.symm, Quiver.Hom.mop, 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ᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y)
          Z).unmop ≅
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z)).unmop)
    (Iso.unmop (α_ X Y Z)) (Iso.symm (α_ Z.unmop Y.unmop X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, CategoryTheory.Iso.symm, 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
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z : Cᴹᵒᵖ } ⟶
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) })
    (Quiver.Hom.mop (Iso.hom (α_ X Y Z))) (Iso.inv (α_ { unmop := Z } { unmop := Y } { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, 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ᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y)
          Z).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z)).unmop)
    (Quiver.Hom.unmop (Iso.hom (α_ X Y Z))) (Iso.inv (α_ Z.unmop Y.unmop X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, 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
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) : Cᴹᵒᵖ } ⟶
      { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z })
    (Quiver.Hom.mop (Iso.inv (α_ X Y Z))) (Iso.hom (α_ { unmop := Z } { unmop := Y } { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, 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ᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X
          (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y Z)).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y)
          Z).unmop)
    (Quiver.Hom.unmop (Iso.inv (α_ X Y Z))) (Iso.hom (α_ Z.unmop Y.unmop X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X : Cᴹᵒᵖ } ≅ { unmop := X })
    (Iso.mop (λ_ X)) (ρ_ { unmop := X })

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 : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
          X).unmop ≅
      X.unmop)
    (Iso.unmop (λ_ X)) (ρ_ X.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, CategoryTheory.Functor.mapIso, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X : Cᴹᵒᵖ } ⟶ { unmop := X })
    (Quiver.Hom.mop (Iso.hom (λ_ X))) (Iso.hom (ρ_ { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
          X).unmop ⟶
      X.unmop)
    (Quiver.Hom.unmop (Iso.hom (λ_ X))) (Iso.hom (ρ_ X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Opposite
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := X : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X })
    (Quiver.Hom.mop (Iso.inv (λ_ X))) (Iso.inv (ρ_ { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl