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
c₁ c₂ c₃ : Cᴹᵒᵖ
d : D
⊢ Eq.{v_2 + 1} (α :=
    @MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ d
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory)
            (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) c₁ c₂) c₃).unmop ⟶
      @MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
        (@MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (@MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ d
            c₃.unmop)
          c₂.unmop)
        c₁.unmop)
    (d ⊴ᵣ Quiver.Hom.unmop (Iso.hom (α_ c₁ c₂ c₃)) ≫
      Iso.hom (αᵣ d (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) c₂ c₃).unmop c₁.unmop) ≫
        Iso.hom (αᵣ d c₃.unmop c₂.unmop) ⊵ᵣ c₁.unmop)
    (Iso.hom (αᵣ d c₃.unmop (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) c₁ c₂).unmop) ≫
      Iso.hom
        (αᵣ
          (@MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ d
            c₃.unmop)
          c₂.unmop c₁.unmop))

Tactic:
simpa only [mop_tensorObj, mop_hom_associator,
      MonoidalRightAction.actionHomRight_inv_hom_assoc] using
      (d ⊴ᵣ (α_ (unmop c₃) (unmop c₂) (unmop c₁)).inv) ≫=
        MonoidalRightAction.actionHom_associator
          (unmop c₃) (unmop c₂) (unmop c₁) d |>.symm

Premises used: CategoryTheory.MonoidalOpposite.unmop, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator, CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight, CategoryTheory.mop_tensorObj, CategoryTheory.mop_hom_associator, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_inv_hom_assoc, CategoryTheory.MonoidalCategoryStruct.associator, Eq.symm, CategoryTheory.whisker_eq, 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 : MonoidalRightAction.{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 _ { unmop := c : Cᴹᵒᵖ }
      d =
    @MonoidalRightActionStruct.actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ d c

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
f : c ⟶ c'
d : D
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ { unmop := c : Cᴹᵒᵖ }
        d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
        { unmop := c' : Cᴹᵒᵖ } d)
    (f.mop ⊵ₗ d) (d ⊴ᵣ 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 : MonoidalRightAction.{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 _ { unmop := c : Cᴹᵒᵖ }
        d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
        { unmop := c : Cᴹᵒᵖ } d')
    ({ unmop := c } ⊴ₗ f) (f ⊵ᵣ c)

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 : c ⟶ c'
g : d ⟶ d'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _ { unmop := c : Cᴹᵒᵖ }
        d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
        { unmop := c' : Cᴹᵒᵖ } d')
    (f.mop ⊙ₗₘ g) (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 : MonoidalRightAction.{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 _
        (tensorObj.{v_1, u_1} (𝒞 := monoidalOppositeCategory) { unmop := c : Cᴹᵒᵖ } { unmop := c' : Cᴹᵒᵖ }) d ≅
      @actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
        { unmop := c : Cᴹᵒᵖ }
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ monoidalOppositeCategory inst_2 toMonoidalCategoryStruct _
          { unmop := c' : Cᴹᵒᵖ } d))
    (αₗ { unmop := c } { unmop := c' } d) (αᵣ d c' c)

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ᵒᵖ
d d' : Dᵒᵖ
f : unop c' ⟶ unop c
g : unop d' ⟶ unop d
a :
  Eq (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d'))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d))))
    (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 d) ≫ Quiver.Hom.op (unop c' ⊴ₗ Quiver.Hom.unop (op g))))
⊢ Eq (α :=
    op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d)) ⟶
      op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d')))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)))
    (Quiver.Hom.op (Quiver.Hom.unop (op f) ⊵ₗ unop d) ≫ Quiver.Hom.op (unop c' ⊴ₗ 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' : Cᵒᵖ
d d' : Dᵒᵖ
f : unop c' ⟶ unop c
g : unop d' ⟶ unop d
⊢ Eq (α :=
    unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d'))) ⟶
      unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d))))
    (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 d) ≫ Quiver.Hom.op (unop c' ⊴ₗ Quiver.Hom.unop (op g))))

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

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def
-- 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₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
a :
  Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
            (unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)))))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (op f) ⊙ₗₘ
            Quiver.Hom.unop (Quiver.Hom.op (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 (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁)) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
          (unop (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂))))))
    (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
      Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂)))))
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
      Quiver.Hom.op
        (Quiver.Hom.unop (op f) ⊙ₗₘ
          Quiver.Hom.unop (Quiver.Hom.op (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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ Iso.hom (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))

Tactic:
haveI := (αₗ (unop _) (unop _) (unop _)).inv ≫=
          MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ Iso.hom (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
    (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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : Cᵒᵖ
d₁ d₂ : Dᵒᵖ
f : unop c₂ ⟶ unop c₁
g : unop c₄ ⟶ unop c₃
h : unop d₂ ⟶ unop d₁
this :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₁)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₃) (unop d₁)))
    (Iso.inv (αₗ (unop c₂) (unop c₄) (unop d₂)) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ (unop c₁) (unop c₃) (unop d₁)))
    (f ⊙ₗₘ g ⊙ₗₘ h)
⊢ Eq (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₂)
            (unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c₄) (unop d₂)))))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c₁ c₃)) (unop d₁))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (op f ⊗ₘ op g) ⊙ₗₘ Quiver.Hom.unop (op h)) ≫
        Iso.hom (Iso.op (Iso.symm (αₗ (unop c₂) (unop c₄) (unop d₂))))))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c₁) (unop c₃) (unop d₁)))) ≫
        Quiver.Hom.op
          (Quiver.Hom.unop (op f) ⊙ₗₘ
            Quiver.Hom.unop (Quiver.Hom.op (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 : MonoidalLeftAction.{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 (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop d))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λₗ (unop d)))) ≫ x))
    (Quiver.Hom.unop
      (Quiver.Hom.op (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) ⊴ₗ x.unop) ≫
        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 (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop d)) ⟶
      d')
    (Iso.hom (Iso.op (Iso.symm (λₗ (unop d)))) ≫ x)
    (Quiver.Hom.op (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) ⊴ₗ x.unop) ≫
      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 : MonoidalLeftAction.{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 (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite))) (unop d))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (λₗ (unop d)))) ≫ x))
    (Quiver.Hom.unop
      (Quiver.Hom.op (unop (tensorUnit.{v_1, u_1} Cᵒᵖ (𝒞 := Category.opposite)) ⊴ₗ x.unop) ≫
        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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' x : Cᵒᵖ
x_1 : c ⟶ c'
x_2 : Dᵒᵖ
a :
  Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c' x)) (unop x_2))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c x)) (unop x_2))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (x_1 ▷ x) ⊵ₗ unop x_2)))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c) (unop x) (unop x_2)))) ≫
        Quiver.Hom.op
            (x_1.unop ⊵ₗ
              unop
                (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x) (unop x_2)))) ≫
          Iso.inv (Iso.op (Iso.symm (αₗ (unop c') (unop x) (unop x_2))))))
⊢ Eq.{v_2 + 1} (α :=
    op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c x)) (unop x_2)) ⟶
      op
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
          (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c' x)) (unop x_2)))
    (Quiver.Hom.op (Quiver.Hom.unop (x_1 ▷ x) ⊵ₗ unop x_2))
    (Iso.hom (Iso.op (Iso.symm (αₗ (unop c) (unop x) (unop x_2)))) ≫
      Quiver.Hom.op
          (x_1.unop ⊵ₗ
            unop
              (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x) (unop x_2)))) ≫
        Iso.inv (Iso.op (Iso.symm (αₗ (unop c') (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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c c' x : Cᵒᵖ
x_1 : c ⟶ c'
x_2 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c' x)) (unop x_2))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) c x)) (unop x_2))))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (x_1 ▷ x) ⊵ₗ unop x_2)))
    (Quiver.Hom.unop
      (Iso.hom (Iso.op (Iso.symm (αₗ (unop c) (unop x) (unop x_2)))) ≫
        Quiver.Hom.op
            (x_1.unop ⊵ₗ
              unop
                (op (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x) (unop x_2)))) ≫
          Iso.inv (Iso.op (Iso.symm (αₗ (unop c') (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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
a :
  Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
          Quiver.Hom.op
            (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3))))))) =
    (Iso.hom
          (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αₗ (unop x) (unop x_1)
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                      (unop x_3)))))))).unop
⊢ Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
      Iso.hom
          (Iso.op (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
        Quiver.Hom.op (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3)))))) =
    Iso.hom
        (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
      Iso.hom
        (Iso.op
          (Iso.symm
            (αₗ (unop x) (unop x_1)
              (unop
                (op
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                    (unop x_3)))))))

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 : MonoidalLeftAction.{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
              (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1) x_2))
            (unop x_3))) ⟶
      unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x)
            (unop
              (op
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_1)
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                        (unop x_3))))))))))
    (inv
      (Quiver.Hom.unop
        (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
          Iso.hom
              (Iso.op
                (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
            Quiver.Hom.op
              (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3)))))))))
    (inv
      (Iso.hom
            (Iso.op
              (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
          Iso.hom
            (Iso.op
              (Iso.symm
                (αₗ (unop x) (unop x_1)
                  (unop
                    (op
                      (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                        (unop x_3)))))))).unop)
⊢ Quiver.Hom.unop
      (Quiver.Hom.op (Quiver.Hom.unop (Iso.hom (α_ x x_1 x_2)) ⊵ₗ unop x_3) ≫
        Iso.hom
            (Iso.op
              (Iso.symm (αₗ (unop x) (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x_1 x_2)) (unop x_3)))) ≫
          Quiver.Hom.op
            (unop x ⊴ₗ Quiver.Hom.unop (Iso.hom (Iso.op (Iso.symm (αₗ (unop x_1) (unop x_2) (unop x_3))))))) =
    (Iso.hom
          (Iso.op (Iso.symm (αₗ (unop (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) x x_1)) (unop x_2) (unop x_3)))) ≫
        Iso.hom
          (Iso.op
            (Iso.symm
              (αₗ (unop x) (unop x_1)
                (unop
                  (op
                    (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop x_2)
                      (unop x_3)))))))).unop

Tactic:
apply IsIso.inv_eq_inv.mp

Premises used: CategoryTheory.IsIso.inv_eq_inv, Iff.mp