awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
smul : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X
one_smul : η ⊵ₗ X ≫ smul = Iso.hom (λₗ X)
mul_smul : μ ⊵ₗ X ≫ smul = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul ≫ smul
smul_1 : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X
one_smul_1 : η ⊵ₗ X ≫ smul_1 = Iso.hom (λₗ X)
mul_smul_1 : μ ⊵ₗ X ≫ smul_1 = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul_1 ≫ smul_1
H :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
mk :
  ∀
    (one_smul_2 :
      Eq.{v₁ + 1} (α :=
        @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
          X)
        (CategoryStruct.comp (Y :=
          @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X) (η ⊵ₗ X)
          (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _))
        (Iso.hom (λₗ X)))
    (mul_smul_2 :
      Eq.{v₁ + 1} (α :=
        @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _
            (tensorObj.{v₁, u₁} (𝒞 := inst) M M) X ⟶
          X)
        (μ ⊵ₗ X ≫ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
        (Iso.hom (αₗ M M X) ≫ M ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)),
    { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } =
      { smul := @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _, one_smul := one_smul_2, mul_smul := mul_smul_2 }
⊢ { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } =
    { smul := smul_1, one_smul := one_smul_1, mul_smul := mul_smul_1 }

Tactic:
subst H
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
smul : @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X
one_smul : η ⊵ₗ X ≫ smul = Iso.hom (λₗ X)
mul_smul : μ ⊵ₗ X ≫ smul = Iso.hom (αₗ M M X) ≫ M ⊴ₗ smul ≫ smul
one_smul_1 :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      X)
    (CategoryStruct.comp (Y :=
      @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X) (η ⊵ₗ X)
      (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _))
    (Iso.hom (λₗ X))
mul_smul_1 :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _
        (tensorObj.{v₁, u₁} (𝒞 := inst) M M) X ⟶
      X)
    (μ ⊵ₗ X ≫ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
    (Iso.hom (αₗ M M X) ≫ M ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
⊢ { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } =
    { smul := @ModObj.smul _ _ _ _ _ _ _ inst_2 _ _, one_smul := one_smul_1, mul_smul := mul_smul_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
rw :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X)
rw₁ :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⊴ₗ e₂.inv ≫ η ⊵ₗ X ≫ e₁.inv ⊵ₗ X)
rw₂ rw₃ :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X) (η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X)

Tactic:
rw [actionHom_def', comp_actionHomLeft, action_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X)

Tactic:
have : η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = _ ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X := by
      rw [actionHom_def', comp_actionHomLeft, action_exchange_assoc]
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
this :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y ⟶ Y)
    (η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom) (Iso.hom (λₗ Y))

Tactic:
simp [reassoc_of% this]
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
rw :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
    ((tensorObj.{v₁, u₁} (𝒞 := inst) N N ⊴ₗ e₂.inv ≫ (e₁.inv ⊗ₘ e₁.inv) ⊵ₗ X) ≫ μ ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)

Tactic:
rw [actionHom_def', action_exchange, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom,
        comp_actionHomLeft, Category.assoc, ← action_exchange, actionHom_def']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange, CategoryTheory.IsMonHom.mul_hom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
nth_rw :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
    (((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv) ≫ μ ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
    ((tensorObj.{v₁, u₁} (𝒞 := inst) N N ⊴ₗ e₂.inv ≫ (e₁.inv ⊗ₘ e₁.inv) ⊵ₗ X) ≫ μ ⊵ₗ X)

Tactic:
nth_rw 2 [action_exchange]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
rw rw₁ :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    ((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv ≫ μ ⊵ₗ X)
    (((e₁.inv ⊗ₘ e₁.inv) ⊵ₗ Y ≫ tensorObj.{v₁, u₁} (𝒞 := inst) M M ⊴ₗ e₂.inv) ≫ μ ⊵ₗ X)

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)

Tactic:
have : μ[N] ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) =
        ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ[M] ⊵ₗ X := by
      rw [actionHom_def', action_exchange, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom,
        comp_actionHomLeft, Category.assoc, ← action_exchange, actionHom_def']
      nth_rw 2 [action_exchange]
      rw [Category.assoc]
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
this :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)
rw :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶ Y)
    (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)
    (Iso.hom (αₗ N N Y) ≫
      N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom) ≫
        (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶ Y)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)
    (Iso.hom (αₗ N N Y) ≫
      N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom) ≫
        (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)

Tactic:
rw [reassoc_of% this]
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
this :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)
rw :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ N
        (@actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (e₁.inv ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X ≫
      M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (N ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₁.inv ⊵ₗ X)
rw₁ rw₂ :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ N
        (@actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (e₁.inv ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X ≫
      M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (e₁.inv ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X ≫
      M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ N
        (@actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (Iso.inv (αₗ N M X) ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ Iso.hom (αₗ M M X) ≫ M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (N ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₁.inv ⊵ₗ X)

Tactic:
rw [← actionHomLeft_action_assoc, action_exchange]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
this :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ N
        (@actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (Iso.inv (αₗ N M X) ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ Iso.hom (αₗ M M X) ≫ M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (N ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₁.inv ⊵ₗ X)

Tactic:
have : (αₗ N M X).inv ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ (αₗ M M X).hom ≫ M ⊴ₗ smul =
        N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X := by
      rw [← actionHomLeft_action_assoc, action_exchange]
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M : C
inst_4 : MonObj M
X : D
N : C
inst_5 : MonObj N
e₁ : M ≅ N
inst_6 : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst_7 : ModObj.{v₁, v₂, u₁, u₂} M X
this_1 :
  Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv)) (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X)
this :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ N
        (@actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X) ⟶
      @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ M X)
    (Iso.inv (αₗ N M X) ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ Iso.hom (αₗ M M X) ≫ M ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _)
    (N ⊴ₗ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₁.inv ⊵ₗ X)
⊢ Eq (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) N N) Y ⟶ Y)
    (((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)
    (Iso.hom (αₗ N N Y) ≫
      N ⊴ₗ ((e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom) ≫
        (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom)

Tactic:
simp [tensorHom_def', actionHom_def', mul_smul_assoc, reassoc_of% this]

Premises used: CategoryTheory.ModObj.mul_smul_assoc, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M X) (η ▷ X) (@smul _ _ _ _ _ _ _ inst_2 _ _))
    (Iso.hom (λ_ X))

Tactic:
ModObj.one_smul (M := M) X

Premises used: CategoryTheory.ModObj.one_smul
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M M) X ⟶ X)
    (μ ▷ X ≫ @smul _ _ _ _ _ _ _ inst_2 _ _)
    (Iso.hom (α_ M M X) ≫
      CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M X)
        (M ◁ @smul _ _ _ _ _ _ _ inst_2 _ _ :
          tensorObj.{v₁, u₁} (𝒞 := inst) M (tensorObj.{v₁, u₁} (𝒞 := inst) M X) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M X)
        (@smul _ _ _ _ _ _ _ inst_2 _ _ :
          @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X))

Tactic:
ModObj.mul_smul (M := M) X

Premises used: CategoryTheory.ModObj.mul_smul
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
X : C
inst_3 : ModObj M X
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) M
        (@MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X) ⟶
      X)
    (M ◁ @smul _ _ _ _ _ _ _ inst_2 _ _ ≫ @smul _ _ _ _ _ _ _ inst_2 _ _)
    (Iso.inv (α_ M M X) ≫ μ ▷ X ≫ @smul _ _ _ _ _ _ _ inst_2 _ _)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M' N' O' : D
A : C
inst_4 : MonObj A
M N O : D
inst_5 : ModObj.{v₁, v₂, u₁, u₂} A M
inst_6 : ModObj.{v₁, v₂, u₁, u₂} A N
inst_7 : ModObj.{v₁, v₂, u₁, u₂} A O
f : M ≅ N
inst_8 : IsModHom.{v₁, v₂, u₁, u₂} A f.hom
⊢ Eq (α := @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A N ⟶ M)
    (@ModObj.smul _ _ _ _ _ _ _ inst_4 _ _ ≫ f.inv) (A ⊴ₗ f.inv ≫ @ModObj.smul _ _ _ _ _ _ _ inst_4 _ _)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
A : C
inst_4 : MonObj A
M : Mod.{v₁, v₂, u₁, u₂} D A
⊢ Eq.{v₂ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A
        (@MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M.X) ⟶
      M.X)
    (A ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_4 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_4 _ _)
    (Iso.inv (αₗ A A M.X) ≫ μ ⊵ₗ M.X ≫ @ModObj.smul _ _ _ _ _ _ _ inst_4 _ _)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
A : C
inst_4 : MonObj A
M N : Mod.{v₁, v₂, u₁, u₂} D A
f₁ f₂ : M ⟶ N
h : f₁.hom = f₂.hom
⊢ f₁ = f₂

Tactic:
Hom.ext h

Premises used: CategoryTheory.Mod.Hom.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
A : C
inst_4 : MonObj A
M : Mod.{v₁, v₂, u₁, u₂} D A
⊢ Hom.hom (𝟙 M) = 𝟙 M.X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
A : C
inst_4 : MonObj A
M N K : Mod.{v₁, v₂, u₁, u₂} D A
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mod
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalLeftAction.{v₁, u₁, v₂, u₂} C D
M' N' O' : D
A_1 : C
inst_4 : MonObj A_1
M_1 N O : D
inst_5 : ModObj.{v₁, v₂, u₁, u₂} A_1 M_1
inst_6 : ModObj.{v₁, v₂, u₁, u₂} A_1 N
inst_7 : ModObj.{v₁, v₂, u₁, u₂} A_1 O
A_2 : C
inst_8 : MonObj A_2
M_2 : Mod.{v₁, v₂, u₁, u₂} D A_2
A B : C
inst_9 : MonObj A
inst_10 : MonObj B
f : A ⟶ B
inst_11 : IsMonHom f
M : D
inst_12 : ModObj.{v₁, v₂, u₁, u₂} B M
rw :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ⟶ M)
    ((η ≫ f) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) (Iso.hom (λₗ M))
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ⟶ M)
    (η ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) (Iso.hom (λₗ M))

Tactic:
rw [← comp_actionHomLeft_assoc]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_assoc