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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
w x : C
y z : D
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.MonoidalLeftAction.id_actionHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x₁ y₁ : C
x₂ y₂ : D
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.MonoidalLeftAction.action_exchange, Eq.rec, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def, 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 : MonoidalLeftAction.{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 _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (Iso.hom (λₗ d) ≫ f ≫ Iso.inv (λₗ d'))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d'))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    ((Iso.hom (λₗ d) ≫ f) ≫ Iso.inv (λₗ d')) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      d')
    (Iso.hom (λₗ d) ≫ f) (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
rw₄ rw₅ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) d ⟶
      d')
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
    (tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f ≫ Iso.hom (λₗ d'))
⊢ Eq (α :=
    d ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorUnit.{v_1, u_1} C (𝒞 := inst))
        d')
    (Iso.inv (λₗ d) ≫ tensorUnit.{v_1, u_1} C (𝒞 := inst) ⊴ₗ f) (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, Eq.comm, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionUnitIso_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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
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.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ≅ y
z : D
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.MonoidalCategory.MonoidalLeftAction.id_actionHomLeft, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
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.MonoidalLeftAction.actionHomRight_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ≅ y
z : D
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.MonoidalLeftAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
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.MonoidalLeftAction.actionHomRight_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp, 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
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.MonoidalLeftAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft, 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
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.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
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.MonoidalLeftAction.id_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
⊢ 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
x' y' : D
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.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
f : x ⟶ y
inst_4 : IsIso f
z : D
⊢ 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 _ 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.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x : C
y z : D
f : y ⟶ z
inst_4 : IsIso f
⊢ Eq (α :=
    @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.MonoidalLeftAction.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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
x y : C
x' y' : D
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.MonoidalLeftAction.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 : MonoidalLeftAction.{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 (α :=
    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 _ X y,
          map := fun {X_1 Y : D} (f : X_1 ⟶ Y) ↦ X ⊴ₗ f, map_id := ⋯, map_comp := ⋯ : Functor.{v_2, v_2, u_2, u_2} D D }
        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) ↦ Y ⊴ₗ f, 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 _ X y,
          map := fun {X_1 Y : D} (f : X_1 ⟶ Y) ↦ X ⊴ₗ f, map_id := ⋯, map_comp := ⋯ : Functor.{v_2, v_2, u_2, u_2} D D }
        x_2 ≫
      f ⊵ₗ x_1)
    (f ⊵ₗ x ≫
      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) ↦ Y ⊴ₗ f, map_id := ⋯, map_comp := ⋯ }
        x_2)

Tactic:
simp [action_exchange]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange
-- 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
⊢ ∀ {c c' d d' : C} (f : d ⟶ d') (g : c ⟶ c'),
    Eq (α := tensorObj.{v_1, u_1} (𝒞 := inst) d c ⟶ tensorObj.{v_1, u_1} (𝒞 := inst) d' c') (f ⊗ₘ g) (f ▷ c ≫ d' ◁ g)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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'
c : C
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d c ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d' c)
    (f ⊙ᵣₘ 𝟙 c) (f ⊵ᵣ c)

Tactic:
simp [actionHom_def]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def
-- 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
c c' : C
f : c ⟶ c'
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d c ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d c')
    (𝟙 d ⊙ᵣₘ f) (d ⊴ᵣ f)

Tactic:
simp [actionHom_def]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_def
-- 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 : D
x y z : C
f : x ⟶ y
g : y ⟶ z
⊢ Eq.{v_2 + 1} (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w x ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ w z)
    (w ⊴ᵣ (f ≫ g)) (w ⊴ᵣ f ≫ w ⊴ᵣ g)

Tactic:
simp [← id_actionHom, ← actionHom_comp]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHom, 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
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
    ((f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ y)) ≫ Iso.inv (ρᵣ y))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst)) (Iso.hom (ρᵣ x) ≫ f ≫ Iso.inv (ρᵣ y))

Tactic:
rw [← Category.assoc, actionUnitIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionUnitIso_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
x y : D
f : x ⟶ y
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ y
        (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
    (f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst))
    ((f ⊵ᵣ tensorUnit.{v_1, u_1} C (𝒞 := inst) ≫ Iso.hom (ρᵣ y)) ≫ Iso.inv (ρᵣ 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
z z' : D
f : z ⟶ z'
x y : C
simp :
  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))
⊢ 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:
simp only [← actionHom_id]

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_id