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' x : C
x_1 : c ⟶ c'
x_2 : D
a :
  Eq.{v_2 + 1} (α :=
    op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c' x)) (op x_2))) ⟶
      op
        (unop
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
            (op (tensorObj.{v_1, u_1} (𝒞 := inst) c x)) (op x_2))))
    (Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (x_1 ▷ x) ⊵ₗ op x_2)))
    (Quiver.Hom.op
      (Iso.hom (Iso.unop (Iso.symm (αₗ (op c) (op x) (op x_2)))) ≫
        Quiver.Hom.unop
            (x_1.op ⊵ₗ
              op
                (unop
                  (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                    (op x) (op x_2)))) ≫
          Iso.inv (Iso.unop (Iso.symm (αₗ (op c') (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 (tensorObj.{v_1, u_1} (𝒞 := inst) c x)) (op x_2)) ⟶
      unop
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
          (op (tensorObj.{v_1, u_1} (𝒞 := inst) c' x)) (op x_2)))
    (Quiver.Hom.unop (Quiver.Hom.op (x_1 ▷ x) ⊵ₗ op x_2))
    (Iso.hom (Iso.unop (Iso.symm (αₗ (op c) (op x) (op x_2)))) ≫
      Quiver.Hom.unop
          (x_1.op ⊵ₗ
            op
              (unop
                (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
                  (op x) (op x_2)))) ≫
        Iso.inv (Iso.unop (Iso.symm (αₗ (op c') (op x) (op x_2)))))

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

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

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

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

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

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

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

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
d : D
⊢ @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c) (op d) =
    op (@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} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c') (op d) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c) (op d))
    (f.op ⊵ₗ op d) (op (f ⊵ₗ d))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, 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.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c) (op d') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c) (op d))
    (op c ⊴ₗ f.op) (op (c ⊴ₗ f))

Tactic:
rfl

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

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, 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} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (op c) (op c')) (op d) ≅
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c)
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op c')
          (op d)))
    (αₗ (op c) (op c') (op d)) (Iso.op (Iso.symm (αₗ 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
c : Cᵒᵖ
d : Dᵒᵖ
⊢ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d) =
    unop (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite 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} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c') (unop d) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d))
    (f.unop ⊵ₗ unop d) (unop (f ⊵ₗ d))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, 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} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop c) (unop d))
    (unop c ⊴ₗ f.unop) (unop (c ⊴ₗ f))

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, 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 : c ⟶ c'
g : d ⟶ d'
⊢ Eq (α :=
    @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) (unop d))
    (f.unop ⊙ₗₘ g.unop) (unop (f ⊙ₗₘ g))

Tactic:
rfl

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

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

Premises used: CategoryTheory.MonoidalOpposite.mop, CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft, 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