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 x_1 x_2 : C
x_3 : x_1 ⟶ x_2
x_4 : D
⊢ 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))))))

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

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

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

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

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

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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d : D
c c' : C
f : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d) (op c') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d) (op c))
    (op d ⊴ᵣ f.op) (op (d ⊴ᵣ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
c c' : C
f : d ⟶ d'
g : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d') (op c') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d) (op c))
    (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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d : D
c c' : C
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite toMonoidalCategoryStruct _ (op d)
        (tensorObj.{v_1, u_1} (𝒞 := Category.opposite) (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'))
    (αᵣ (op d) (op c) (op c')) (Iso.op (Iso.symm (αᵣ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d : Dᵒᵖ
c : Cᵒᵖ
⊢ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c) =
    unop (@actionObj.{v_1, u_1, v_2, u_2} _ _ Category.opposite Category.opposite 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ᵒᵖ
d d' : Dᵒᵖ
f : d ⟶ d'
c : Cᵒᵖ
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))
    (f.unop ⊵ᵣ unop c) (unop (f ⊵ᵣ c))

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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d : Dᵒᵖ
c c' : Cᵒᵖ
f : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))
    (unop d ⊴ᵣ f.unop) (unop (d ⊴ᵣ 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d d' : Dᵒᵖ
c c' : Cᵒᵖ
f : d ⟶ d'
g : c ⟶ c'
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d') (unop c') ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d) (unop c))
    (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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} Cᵒᵖ Dᵒᵖ
d : Dᵒᵖ
c c' : Cᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _ (unop d)
        (tensorObj.{v_1, u_1} (𝒞 := inst) (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'))
    (αᵣ (unop d) (unop c) (unop c')) (Iso.unop (Iso.symm (αᵣ d c c')))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).right ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).right)
    (Arrow.Hom.right ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.right (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))

Tactic:
simp [whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
refine :
  Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) X₁ X₂ ⟶ tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂)
    ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
refine Arrow.hom_ext _ _ ?_ (by simp [whisker_exchange_assoc])

Premises used: CategoryTheory.Arrow.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
h₀ :
  Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))
h₁ :
  Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.right ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))) (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂))

Tactic:
apply pushout.hom_ext

Premises used: CategoryTheory.Limits.pushout.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))

Tactic:
simp [whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc