awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
z z' : D
f : z ⟶ z'
x y : C
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
    (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ Iso.hom (αᵣ z' x y)) ≫ Iso.inv (αᵣ z' x y))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
    (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (Iso.hom (αᵣ z x y) ≫ ((f ⊙ᵣₘ 𝟙 x) ⊙ᵣₘ 𝟙 y) ≫ Iso.inv (αᵣ z' x y))

Tactic:
rw [← Category.assoc, ← actionAssocIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
z z' : D
f : z ⟶ z'
x y : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ z'
        (tensorObj.{v_1, u_1} (𝒞 := inst) x y))
    (f ⊙ᵣₘ 𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst) x y)) (((f ⊙ᵣₘ 𝟙 x ⊗ₘ 𝟙 y) ≫ Iso.hom (αᵣ z' x y)) ≫ Iso.inv (αᵣ z' x y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
w x y : D
f : w ⟶ x
g : x ⟶ y
z : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
    ((f ≫ g) ⊵ᵣ z) (f ⊵ᵣ z ≫ g ⊵ᵣ z)

Tactic:
simp only [← actionHom_id, ← actionHom_comp, Category.id_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
y : D
z x x' : C
f : x ⟶ x'
⊢ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⊴ᵣ f =
    Iso.inv (αᵣ y z x) ≫ y ⊴ᵣ z ◁ f ≫ Iso.hom (αᵣ y z x')

Tactic:
simp [whiskerRight_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.whiskerRight_actionHomLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
w x : D
y z : C
f : w ⟶ x
g : y ⟶ z
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w y ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (w ⊴ᵣ g ≫ f ⊵ᵣ z) (f ⊵ᵣ y ≫ x ⊴ᵣ g)

Tactic:
simp only [← id_actionHom, ← actionHom_id, ← actionHom_comp, id_comp, comp_id]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x₁ y₁ : D
x₂ y₂ : C
f : x₁ ⟶ y₁
g : x₂ ⟶ y₂
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x₁ x₂ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y₁ y₂)
    (f ⊙ᵣₘ g) (x₁ ⊴ᵣ g ≫ f ⊵ᵣ y₂)

Tactic:
action_exchange f g ▸ actionHom_def f g

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def, Eq.rec, CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d d' : D
f : d ⟶ d'
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ d) ≫ f ≫ Iso.inv (ρᵣ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    ((Iso.hom (ρᵣ d) ≫ f) ≫ Iso.inv (ρᵣ d')) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      d')
    (Iso.hom (ρᵣ d) ≫ f) (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
rw₄ rw₅ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      d')
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d'
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (Iso.inv (ρᵣ d) ≫ f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (f ≫ Iso.inv (ρᵣ d'))

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Eq.comm, Iso.comp_inv_eq, actionUnitIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_hom_naturality, Eq.comm
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ≅ z
rw : x ⊴ᵣ (f.hom ≫ f.inv) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₁ : x ⊴ᵣ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
⊢ x ⊴ᵣ f.hom ≫ x ⊴ᵣ f.inv = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)

Tactic:
rw [← actionHomRight_comp, Iso.hom_inv_id, actionHomRight_id]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
rw : (f.hom ≫ f.inv) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : 𝟙 x ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
⊢ f.hom ⊵ᵣ z ≫ f.inv ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)

Tactic:
rw [← comp_actionHomLeft, Iso.hom_inv_id, id_actionHomLeft]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ≅ z
rw : x ⊴ᵣ (f.inv ≫ f.hom) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : x ⊴ᵣ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
⊢ x ⊴ᵣ f.inv ≫ x ⊴ᵣ f.hom = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)

Tactic:
rw [← actionHomRight_comp, Iso.inv_hom_id, actionHomRight_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ≅ y
z : C
rw : (f.inv ≫ f.hom) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₁ : 𝟙 y ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
⊢ f.inv ⊵ᵣ z ≫ f.hom ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)

Tactic:
rw [← comp_actionHomLeft, Iso.inv_hom_id, id_actionHomLeft]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ᵣ (f ≫ inv f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₁ : x ⊴ᵣ 𝟙 y = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y))
⊢ x ⊴ᵣ f ≫ x ⊴ᵣ inv f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)

Tactic:
rw [← actionHomRight_comp, IsIso.hom_inv_id, actionHomRight_id]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
rw : (f ≫ inv f) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : 𝟙 x ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
⊢ f ⊵ᵣ z ≫ inv f ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)

Tactic:
rw [← comp_actionHomLeft, IsIso.hom_inv_id, id_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ⟶ z
inst_4 : IsIso f
rw : x ⊴ᵣ (inv f ≫ f) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₁ : x ⊴ᵣ 𝟙 z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z))
⊢ x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)

Tactic:
rw [← actionHomRight_comp, IsIso.inv_hom_id, actionHomRight_id]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_comp, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_id
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
rw : (inv f ≫ f) ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₁ : 𝟙 y ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
rw₂ rw₃ :
  Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
    (𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z))
⊢ inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)

Tactic:
rw [← comp_actionHomLeft, IsIso.inv_hom_id, id_actionHomLeft]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalRightAction.comp_actionHomLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
⊢ f ⊵ᵣ z ≫ inv f ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z) ∧
    inv f ⊵ᵣ z ≫ f ⊵ᵣ z = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ⟶ z
inst_4 : IsIso f
⊢ x ⊴ᵣ f ≫ x ⊴ᵣ inv f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y) ∧
    x ⊴ᵣ inv f ≫ x ⊴ᵣ f = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
x' y' : C
f : x ⟶ y
g : x' ⟶ y'
inst_4 : IsIso f
inst_5 : IsIso g
⊢ (f ⊙ᵣₘ g) ≫ (inv f ⊙ᵣₘ inv g) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x x') ∧
    (inv f ⊙ᵣₘ inv g) ≫ (f ⊙ᵣₘ g) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y y')

Tactic:
simp [← actionHom_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
f : x ⟶ y
inst_4 : IsIso f
z : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z)
    (inv (f ⊵ᵣ z)) (inv f ⊵ᵣ z)

Tactic:
IsIso.inv_eq_of_hom_inv_id <| hom_inv_actionHomLeft' f z

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.hom_inv_actionHomLeft'
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : D
y z : C
f : y ⟶ z
inst_4 : IsIso f
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x z ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x y)
    (inv (x ⊴ᵣ f)) (x ⊴ᵣ inv f)

Tactic:
IsIso.inv_eq_of_hom_inv_id <| actionHomRight_hom_inv' x f

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomRight_hom_inv'
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x y : D
x' y' : C
f : x ⟶ y
g : x' ⟶ y'
inst_4 : IsIso f
inst_5 : IsIso g
⊢ (f ⊙ᵣₘ g) ≫ (inv f ⊙ᵣₘ inv g) = 𝟙 (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x x')

Tactic:
simp [← actionHom_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
X Y : C
f : X ⟶ Y
x x_1 : D
x_2 : x ⟶ x_1
⊢ Eq (α :=
    Quiver.Hom (V := D)
      (Functor.obj.{v_2, v_2, u_2, u_2}
        { obj := fun (y : D) ↦ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y X,
          map := fun {X_1 Y : D} (f : X_1 ⟶ Y) ↦ f ⊵ᵣ X, map_id := ⋯, map_comp := ⋯ }
        x)
      (Functor.obj.{v_2, v_2, u_2, u_2}
        { obj := fun (y : D) ↦ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y Y,
          map := fun {X Y_1 : D} (f : X ⟶ Y_1) ↦ f ⊵ᵣ Y, map_id := ⋯, map_comp := ⋯ }
        x_1))
    (Functor.map
        { obj := fun (y : D) ↦ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y X,
          map := fun {X_1 Y : D} (f : X_1 ⟶ Y) ↦ f ⊵ᵣ X, map_id := ⋯, map_comp := ⋯ : Functor.{v_2, v_2, u_2, u_2} D D }
        x_2 ≫
      x_1 ⊴ᵣ f)
    (x ⊴ᵣ f ≫
      Functor.map
        { obj := fun (y : D) ↦ @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y Y,
          map := fun {X Y_1 : D} (f : X ⟶ Y_1) ↦ f ⊵ᵣ Y, map_id := ⋯, map_comp := ⋯ }
        x_2)

Tactic:
simp [action_exchange]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.action_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Action.End
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} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (MonoidalOpposite.unmop (Functor.obj (curriedActionMop C D) c)) d ⟶
      Functor.obj.{v_2, v_2, u_2, u_2} (MonoidalOpposite.unmop (Functor.obj (curriedActionMop C D) c')) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.map (curriedActionMop C D) f)) d) (f ⊵ₗ d)

Tactic:
rfl

Premises used: rfl