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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : Cᵒᵖ
x_1 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x)))))
    (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x)))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x)))
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
          (unop
            (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x))) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x)))
    (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x))))
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
      Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x))

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 : Cᵒᵖ
x_1 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))
                x)))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
    (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x))))))
    (inv
      (Quiver.Hom.unop
        (Iso.hom
            (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
          Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x))))
⊢ Eq.{v_2 + 1} (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) x)))))
    (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x)))))
    (Quiver.Hom.unop
      (Iso.hom
          (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
        Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x)))

Tactic:
apply IsIso.inv_eq_inv.mp

Premises used: CategoryTheory.IsIso.inv_eq_inv, Iff.mp
-- 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 : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))
                x)))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
    (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (λ_ x))))))
    (inv
      (Quiver.Hom.unop
        (Iso.hom
            (Iso.op (Iso.symm (αᵣ (unop x_1) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop x)))) ≫
          Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (ρᵣ (unop x_1))))) ⊵ᵣ unop x))))

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 : Cᵒᵖ
x_1 : Dᵒᵖ
a :
  Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x)))) =
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (ρᵣ
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                      (unop x)))))))).unop
⊢ Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x))) =
    Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (ρᵣ
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x)))))))

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 : Cᵒᵖ
x_1 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x
                (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
    (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x))))))
    (inv
      (Iso.hom
            (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
          Iso.hom
            (Iso.op
              (Iso.symm
                (ρᵣ
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                        (unop x)))))))).unop)
⊢ Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x)))) =
    (Iso.hom (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (ρᵣ
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                      (unop x)))))))).unop

Tactic:
apply IsIso.inv_eq_inv.mp

Premises used: CategoryTheory.IsIso.inv_eq_inv, Iff.mp
-- 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 : Cᵒᵖ
x_1 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
            (unop
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x
                (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1) (unop x))))
    (inv (Quiver.Hom.unop (Quiver.Hom.op (unop x_1 ⊴ᵣ Quiver.Hom.unop (Iso.hom (ρ_ x))))))
    (inv
      (Iso.hom
            (Iso.op (Iso.symm (αᵣ (unop x_1) (unop x) (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)))))) ≫
          Iso.hom
            (Iso.op
              (Iso.symm
                (ρᵣ
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                        (unop x)))))))).unop)

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ᵒᵖ
c c' : C
d d' : D
f : d ⟶ d'
g : c ⟶ c'
a :
  Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op c'))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
            (op c))))
    (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op c)))
        (Quiver.Hom.unop (f.op ⊵ᵣ op c)) (Quiver.Hom.unop (op d' ⊴ᵣ g.op))))
⊢ Eq.{v_2 + 1} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
          (op c)) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c')))
    (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op))
    (CategoryStruct.comp (Y :=
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op c)))
      (Quiver.Hom.unop (f.op ⊵ᵣ op c)) (Quiver.Hom.unop (op d' ⊴ᵣ g.op)))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_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 : d ⟶ d'
g : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op c'))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
            (op c))))
    (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op c)))
        (Quiver.Hom.unop (f.op ⊵ᵣ op c)) (Quiver.Hom.unop (op d' ⊴ᵣ g.op))))

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

Premises used: Quiver.Hom.op, 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 : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
a :
  Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op d₂) (op c₂))))
            (op c₄))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)))))
    (Quiver.Hom.op
      (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄))))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)) ⊙ᵣₘ h.op)))
⊢ Eq.{v_2 + 1} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op
            (unop
              (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                (op d₂) (op c₂))))
          (op c₄)))
    (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄)))))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
      Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)) ⊙ᵣₘ h.op))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_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 : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
          (op c₂))
        (op c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op c₁))
        (op c₃))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ Iso.hom (αᵣ (op d₂) (op c₂) (op c₄)) ≫ ((f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op))

Tactic:
haveI := (αᵣ (op _) (op _) (op _)).inv ≫=
      MonoidalRightAction.actionAssocIso_hom_naturality f.op g.op h.op
-- 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 : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
this :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
          (op c₂))
        (op c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op c₁))
        (op c₃))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ Iso.hom (αᵣ (op d₂) (op c₂) (op c₄)) ≫ ((f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op))
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
          (op c₂))
        (op c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op c₁))
        (op c₃))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
    ((f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op)

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 : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
this :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₂)
          (op c₂))
        (op c₄) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
          (op c₁))
        (op c₃))
    (Iso.inv (αᵣ (op d₂) (op c₂) (op c₄)) ≫ (f.op ⊙ᵣₘ g.op ⊗ₘ h.op) ≫ Iso.hom (αᵣ (op d₁) (op c₁) (op c₃)))
    ((f.op ⊙ᵣₘ g.op) ⊙ᵣₘ h.op)
⊢ Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op d₂) (op c₂))))
            (op c₄))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d₁)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)))))
    (Quiver.Hom.op
      (Quiver.Hom.unop (f.op ⊙ᵣₘ Quiver.Hom.op (g ⊗ₘ h)) ≫ Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₂) (op c₂) (op c₄))))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op d₁) (op c₁) (op c₃)))) ≫
        Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (f.op ⊙ᵣₘ g.op)) ⊙ᵣₘ h.op)))

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 (α :=
    op d' ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
            (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
    (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op d)))) ≫ x))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))
        (Quiver.Hom.unop (x.op ⊵ᵣ op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op d')))))))
⊢ Eq (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) ⟶
      d')
    (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op d)))) ≫ x)
    (CategoryStruct.comp (Y :=
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
          (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))
      (Quiver.Hom.unop (x.op ⊵ᵣ op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op d'))))))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_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 (α :=
    op d' ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
            (op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
    (Quiver.Hom.op (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op d)))) ≫ x))
    (Quiver.Hom.op
      (CategoryStruct.comp (Y :=
        unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d')
            (op (tensorUnit.{v_1, u_1} C (𝒞 := inst)))))
        (Quiver.Hom.unop (x.op ⊵ᵣ op (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Iso.hom (Iso.unop (Iso.symm (ρᵣ (op 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} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_2)))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1)))))
    (Quiver.Hom.op (Quiver.Hom.unop (op x_4 ⊴ᵣ Quiver.Hom.op (x ◁ x_3))))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_1)))) ≫
        Quiver.Hom.unop
            (op
                (unop
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                    (op x_4) (op x))) ⊴ᵣ
              x_3.op) ≫
          Iso.inv (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_2))))))
⊢ Eq.{v_2 + 1} (α :=
    unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_1))) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op x_4)
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) x x_2))))
    (Quiver.Hom.unop (op x_4 ⊴ᵣ Quiver.Hom.op (x ◁ x_3)))
    (Iso.hom (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_1)))) ≫
      Quiver.Hom.unop
          (op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x_4) (op x))) ⊴ᵣ
            x_3.op) ≫
        Iso.inv (Iso.unop (Iso.symm (αᵣ (op x_4) (op x) (op x_2)))))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj