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
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)
    (CategoryStruct.comp (Y := @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ B M) (η ⊵ₗ M)
      (@ModObj.smul _ _ _ _ _ _ _ inst_10 _ _))
    (Iso.hom (λₗ M))
rw₁ rw₂ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ⟶ M)
    (Iso.hom (λₗ M)) (Iso.hom (λₗ M))
⊢ 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))

Tactic:
rw [IsMonHom.one_hom, ModObj.one_smul]

Premises used: CategoryTheory.IsMonHom.one_hom, CategoryTheory.ModObj.one_smul
-- 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
a :
  f ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M ≫
    B ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
| A ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) ≫ f ⊵ₗ M

Tactic:
rw [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' 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
slice_rhs :
  μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ =
    Iso.hom (αₗ A A M) ≫
      (f ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M ≫
          B ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)) ≫
        @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    (Iso.hom (αₗ A A M) ≫
      A ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)

Tactic:
slice_rhs 2 3 => rw [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' 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
simp :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫
      Iso.hom (αₗ B A M) ≫
        B ⊴ₗ f ⊵ₗ M ≫ B ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ =
    Iso.hom (αₗ A A M) ≫
      (f ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M ≫
          B ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)) ≫
        @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _

Tactic:
simp only [actionHomLeft_action_assoc, Category.assoc, Iso.hom_inv_id_assoc,
      actionHomRight_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_action_assoc, CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp, CategoryTheory.Iso.hom_inv_id_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' 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
a : Iso.inv (αₗ B B M) ≫ μ ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _
| B ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _

Tactic:
rw [ModObj.assoc_flip]

Premises used: CategoryTheory.ModObj.assoc_flip
-- 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
slice_rhs :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫
      Iso.hom (αₗ B A M) ≫ B ⊴ₗ f ⊵ₗ M ≫ Iso.inv (αₗ B B M) ≫ μ ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫
      Iso.hom (αₗ B A M) ≫
        B ⊴ₗ f ⊵ₗ M ≫ B ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)

Tactic:
slice_rhs 4 6 => rw [ModObj.assoc_flip]

Premises used: CategoryTheory.ModObj.assoc_flip
-- 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
a : (B ◁ f) ⊵ₗ M
| Iso.hom (αₗ B A M) ≫ B ⊴ₗ f ⊵ₗ M ≫ Iso.inv (αₗ B B M)

Tactic:
rw [← whiskerLeft_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft
-- 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
slice_rhs :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫ ((B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫
      Iso.hom (αₗ B A M) ≫ B ⊴ₗ f ⊵ₗ M ≫ Iso.inv (αₗ B B M) ≫ μ ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)

Tactic:
slice_rhs 2 4 => rw [← whiskerLeft_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft
-- 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
a : (f ▷ A ≫ B ◁ f) ⊵ₗ M
| (f ▷ A) ⊵ₗ M ≫ (B ◁ f) ⊵ₗ M

Tactic:
rw [← comp_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft
-- 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
slice_rhs :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    (((f ▷ A ≫ B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A) ⊵ₗ M ≫ ((B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)

Tactic:
slice_rhs 1 2 => rw [← comp_actionHomLeft]

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft
-- 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 _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    (((f ▷ A ≫ B ◁ f) ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
rw₁ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
rw₂ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    ((μ ≫ f) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
rw₃ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (((f ⊗ₘ f) ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
rw₄ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (((f ▷ A ≫ B ◁ f) ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
rw₅ rw₆ :
  Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    ((f ▷ A ≫ B ◁ f ≫ μ) ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
⊢ Eq.{v₂ + 1} (α :=
    @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ (tensorObj.{v₁, u₁} (𝒞 := inst) A A) M ⟶ M)
    (μ ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
    (((f ▷ A ≫ B ◁ f) ⊵ₗ M ≫ μ ⊵ₗ M) ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)

Tactic:
rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.IsMonHom.mul_hom, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft, CategoryTheory.MonoidalCategory.MonoidalLeftAction.comp_actionHomLeft_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
A B : C
inst_4 : MonObj A
inst_5 : MonObj B
f : A ⟶ B
inst_6 : IsMonHom f
M N : D
inst_7 : ModObj.{v₁, v₂, u₁, u₂} B M
inst_8 : ModObj.{v₁, v₂, u₁, u₂} B N
g : M ⟶ N
inst_9 : IsModHom.{v₁, v₂, u₁, u₂} B g
this_1 : ModObj.{v₁, v₂, u₁, u₂} A M := scalarRestriction f M
this : ModObj.{v₁, v₂, u₁, u₂} A N := scalarRestriction f N
⊢ Eq (α := @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M ⟶ N)
    (@ModObj.smul _ _ _ _ _ _ _ inst_4 _ _ ≫ g) (A ⊴ₗ g ≫ @ModObj.smul _ _ _ _ _ _ _ inst_4 _ _)

Tactic:
simpa using (action_exchange_assoc f g γ).symm

Premises used: CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc, CategoryTheory.ModObj.smul, Eq.symm
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      ((η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶ X)
    ((η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) (Iso.hom (λ_ X))

Tactic:
rw [← cancel_epi (λ_ X).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (η ▷ X ≫ M ◁ e.inv ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X))
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      ((η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X))

Tactic:
simp only [comp_whiskerRight, tensorHom_def, Category.assoc,
      hom_inv_whiskerRight_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (η ▷ X ≫ M ◁ e.inv ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) (Iso.inv (λ_ X))
      (Iso.hom (λ_ X))

Tactic:
simp [← tensorHom_def_assoc, leftUnitor_inv_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
rw :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (Iso.hom (ρ_ X))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X)
    (X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) (Iso.hom (ρ_ X))

Tactic:
rw [← cancel_epi (ρ_ X).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
simp :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (X ◁ η ≫ e.inv ▷ M ≫ μ ≫ e.hom) =
    𝟙 X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (Iso.hom (ρ_ X))

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp, tensorHom_def', Category.assoc,
      whiskerLeft_hom_inv_assoc, Iso.inv_hom_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (X ◁ η ≫ e.inv ▷ M ≫ μ ≫ e.hom) =
    𝟙 X

Tactic:
simp [← tensorHom_def'_assoc, rightUnitor_inv_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.rightUnitor_inv_comp_tensorHom_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
e : M ≅ X
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X X) X ⟶ X)
    (((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom)
    (Iso.hom (α_ X X X) ≫ X ◁ ((e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom)

Tactic:
simpa [← id_tensorHom, ← tensorHom_id,
      -associator_conjugation, associator_naturality_assoc] using
      congr(((e.inv ⊗ₘ e.inv) ⊗ₘ e.inv) ≫ $(MonObj.mul_assoc M) ≫ e.hom)

Premises used: CategoryTheory.MonObj.mul_assoc, CategoryTheory.MonoidalCategory.associator_naturality_assoc, CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategoryStruct.tensorHom, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.MonoidalCategory.associator_conjugation, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
⊢ tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M X Y : C
inst_2 : MonObj M
⊢ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom
        (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))
          (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
monoidal_coherence
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : MonObj X
H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
mk :
  ∀ (one : tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) (mul : tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X)
    (one_mul : one ▷ X ≫ mul = Iso.hom (λ_ X)) (mul_one : X ◁ one ≫ mul = Iso.hom (ρ_ X))
    (mul_assoc : mul ▷ X ≫ mul = Iso.hom (α_ X X X) ≫ X ◁ mul ≫ mul)
    (H : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ)
    (this : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η),
    { one := one, mul := mul, one_mul := one_mul, mul_one := mul_one, mul_assoc := mul_assoc : MonObj X } = h₂
⊢ h₁ = h₂

Tactic:
cases h₁