awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ : Cᴹᵒᵖ
d : D
⊢ Quiver.Hom.unmop (Iso.hom (α_ c₁ c₂ c₃)) ⊵ₗ d ≫
      Iso.hom (αₗ (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) c₂ c₃).unmop c₁.unmop d) ≫
        Iso.hom
          (αₗ c₃.unmop c₂.unmop
            (@MonoidalLeftActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
              c₁.unmop d)) =
    Iso.hom (αₗ c₃.unmop (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) c₁ c₂).unmop d) ≫
      c₃.unmop ⊴ₗ Iso.hom (αₗ c₂.unmop c₁.unmop d)

Tactic:
simpa only [mop_tensorObj, mop_hom_associator,
      MonoidalLeftAction.inv_hom_actionHomLeft_assoc] using
      (α_ (unmop c₃) (unmop c₂) (unmop c₁)).inv ⊵ₗ d ≫=
        MonoidalLeftAction.associator_actionHom
          (unmop c₃) (unmop c₂) (unmop c₁) d |>.symm

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft, CategoryTheory.MonoidalOpposite.unmop, CategoryTheory.mop_tensorObj, CategoryTheory.mop_hom_associator, CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom, CategoryTheory.MonoidalCategoryStruct.associator, Eq.symm, CategoryTheory.whisker_eq, CategoryTheory.MonoidalCategory.MonoidalLeftAction.inv_hom_actionHomLeft_assoc, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c : C
d : D
⊢ @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
      { unmop := c : Cᴹᵒᵖ } =
    @MonoidalLeftActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ c d

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' : C
f : c ⟶ c'
d : D
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
        { unmop := c : Cᴹᵒᵖ } ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
        { unmop := c' : Cᴹᵒᵖ })
    (d ⊴ᵣ f.mop) (f ⊵ₗ d)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c : C
d d' : D
f : d ⟶ d'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
        { unmop := c : Cᴹᵒᵖ } ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d'
        { unmop := c : Cᴹᵒᵖ })
    (f ⊵ᵣ { unmop := c }) (c ⊴ₗ f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' : D
d d' : C
f : c ⟶ c'
g : d ⟶ d'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ c
        { unmop := d : Cᴹᵒᵖ } ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ c'
        { unmop := d' : Cᴹᵒᵖ })
    (f ⊙ᵣₘ g.mop) (g ⊙ₗₘ f)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' : C
d : D
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := c : Cᴹᵒᵖ } { unmop := c' : Cᴹᵒᵖ }) ≅
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ d
          { unmop := c : Cᴹᵒᵖ })
        { unmop := c' : Cᴹᵒᵖ })
    (αᵣ d { unmop := c } { unmop := c' }) (αₗ c' c d)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
c c' : Cᵒᵖ
d d' : Dᵒᵖ
f : unop d' ⟶ unop d
g : unop c' ⟶ unop c
a :
  Eq (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c'))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ᵣ unop c) ≫ Quiver.Hom.op (unop d' ⊴ᵣ Quiver.Hom.unop (op g))))
⊢ Eq (α :=
    op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c)) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c')))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ᵣ unop c) ≫ Quiver.Hom.op (unop d' ⊴ᵣ Quiver.Hom.unop (op g)))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
c c' : Cᵒᵖ
d d' : Dᵒᵖ
f : unop d' ⟶ unop d
g : unop c' ⟶ unop c
⊢ Eq (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c'))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ᵣ unop c) ≫ Quiver.Hom.op (unop d' ⊴ᵣ Quiver.Hom.unop (op g))))

Tactic:
simpa [MonoidalRightAction.action_exchange] using
          MonoidalRightAction.actionHom_def f g

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def, CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
a :
  Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
            (unop c₄))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g))) ⊙ᵣₘ
            Quiver.Hom.unop (op h))))
⊢ Eq (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃))) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
          (unop c₄)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄)))))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g))) ⊙ᵣₘ
          Quiver.Hom.unop (op h)))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ Iso.hom (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))

Tactic:
haveI := (αᵣ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalRightAction.actionAssocIso_hom_naturality f g h
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ Iso.hom (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h)

Tactic:
simp only [Iso.inv_hom_id_assoc] at this

Premises used: CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : Dᵒᵖ
c₁ c₂ c₃ c₄ : Cᵒᵖ
f : unop d₂ ⟶ unop d₁
g : unop c₂ ⟶ unop c₁
h : unop c₄ ⟶ unop c₃
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂)) (unop c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁) (unop c₁)) (unop c₃))
    (Iso.inv (αᵣ (unop d₂) (unop c₂) (unop c₄)) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ (unop d₁) (unop c₁) (unop c₃)))
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₂) (unop c₂))))
            (unop c₄))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d₁)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g ⊗ₘ op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₂) (unop c₂) (unop c₄))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop d₁) (unop c₁) (unop c₃)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ᵣₘ Quiver.Hom.unop (op g))) ⊙ᵣₘ
            Quiver.Hom.unop (op h))))

Tactic:
simp [← this]
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : Dᵒᵖ
x : d ⟶ d'
a :
  Eq (α :=
    unop d' ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} C _ inst inst_2 toMonoidalCategoryStruct _ (unop d)
            (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d)))) ≫ x))
    (Quiver.Hom.unop
      (Quiver.Hom.op (x.unop ⊵ᵣ unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) ≫
        Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d'))))))
⊢ Eq (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} C _ inst inst_2 toMonoidalCategoryStruct _ (unop d)
          (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))) ⟶
      d')
    (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d)))) ≫ x)
    (Quiver.Hom.op (x.unop ⊵ᵣ unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) ≫
      Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d')))))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : Dᵒᵖ
x : d ⟶ d'
⊢ Eq (α :=
    unop d' ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} C _ inst inst_2 toMonoidalCategoryStruct _ (unop d)
            (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d)))) ≫ x))
    (Quiver.Hom.unop
      (Quiver.Hom.op (x.unop ⊵ᵣ unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) ≫
        Iso.hom (Iso.op (Iso.symm (ρᵣ (unop d'))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : x_1 ⟶ x_2
x_4 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_2)))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)))))
    (Quiver.Hom.unop (Quiver.Hom.op (unop x_4 ⊴ᵣ Quiver.Hom.unop (x ◁ x_3))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_1)))) ≫
        Quiver.Hom.op
            (unop
                (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4) (unop x))) ⊴ᵣ
              x_3.unop) ≫
          Iso.inv (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_2))))))
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1))) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_2))))
    (Quiver.Hom.op (unop x_4 ⊴ᵣ Quiver.Hom.unop (x ◁ x_3)))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_1)))) ≫
      Quiver.Hom.op
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4) (unop x))) ⊴ᵣ
            x_3.unop) ≫
        Iso.inv (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_2)))))

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : x_1 ⟶ x_2
x_4 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_2)))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4)
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)))))
    (Quiver.Hom.unop (Quiver.Hom.op (unop x_4 ⊴ᵣ Quiver.Hom.unop (x ◁ x_3))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_1)))) ≫
        Quiver.Hom.op
            (unop
                (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_4) (unop x))) ⊴ᵣ
              x_3.unop) ≫
          Iso.inv (Iso.op (Iso.symm (αᵣ (unop x_4) (unop x) (unop x_2))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop
              (op
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1))))
            (unop x_2))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)
                x_2)))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
          Iso.hom
            (Iso.op
              (Iso.symm
                (αᵣ
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1) (unop x_2))))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ unop x_2)))
⊢ Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
      Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αᵣ
                (unop
                  (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                (unop x_1) (unop x_2)))) =
    Iso.hom
        (Iso.op (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ unop x_2)

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Opposites
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)
                x_2)))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop
              (op
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3) (unop x))))
                  (unop x_1))))
            (unop x_2))))
    (inv
      (Quiver.Hom.unop
        (Quiver.Hom.op (unop x_3 ⊴ᵣ Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2))) ≫
          Iso.hom
              (Iso.op
                (Iso.symm (αᵣ (unop x_3) (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2))))) ≫
            Iso.hom
              (Iso.op
                (Iso.symm
                  (αᵣ
                    (unop
                      (op
                        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_3)
                          (unop x))))
                    (unop x_1) (unop x_2)))))))
    (inv
      (Quiver.Hom.unop
        (Iso.hom
            (Iso.op
              (Iso.symm (αᵣ (unop x_3) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2)))) ≫
          Quiver.Hom.op
            (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_3) (unop x) (unop x_1))))) ⊵ᵣ unop x_2))))

Tactic:
simp