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
x x_1 x_2 : Cᵒᵖ
x_3 : Dᵒᵖ
⊢ Eq.{v_2 + 1} (α :=
    unop
        (op
          (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_2 toMonoidalCategoryStruct _
            (unop
              (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)

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

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

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

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

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

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

Tactic:
simp