awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) ≫ f ⊵ₗ M
have a : f ⊵ₗ @actionObj.{v₁, u₁, v₂, u₂} _ _ inst inst_2 toMonoidalCategoryStruct _ A M ≫
  B ⊴ₗ (f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _)
Tactic: rw [action_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ 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 _ _)
have 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 _ _
Tactic: slice_rhs 2 3 => rw [action_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ μ ⊵ₗ 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 _ _
have 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 _ _)
Tactic: simp only [actionHomLeft_action_assoc, Category.assoc, Iso.hom_inv_id_assoc,
      actionHomRight_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
| B ⊴ₗ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _ ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _
have a : Iso.inv (αₗ B B M) ≫ μ ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _
Tactic: rw [ModObj.assoc_flip]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ 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 _ _)
have 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 _ _)
Tactic: slice_rhs 4 6 => rw [ModObj.assoc_flip]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
| Iso.hom (αₗ B A M) ≫ B ⊴ₗ f ⊵ₗ M ≫ Iso.inv (αₗ B B M)
have a : (B ◁ f) ⊵ₗ M
Tactic: rw [← whiskerLeft_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ 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 _ _)
have 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 _ _)
Tactic: slice_rhs 2 4 => rw [← whiskerLeft_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
| (f ▷ A) ⊵ₗ M ≫ (B ◁ f) ⊵ₗ M
have a : (f ▷ A ≫ B ◁ f) ⊵ₗ M
Tactic: rw [← comp_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ 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 _ _)
have 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 _ _)
Tactic: slice_rhs 1 2 => rw [← comp_actionHomLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 _ _)
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 _ _)
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 _ _)
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 _ _)
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (goal)
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 _ _)
⊢ 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 _ _)
have 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 _ _)
Tactic: rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶ X)
    ((η ≫ e.hom) ▷ X ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) (Iso.hom (λ_ X))
have 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))
Tactic: rw [← cancel_epi (λ_ X).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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))
      ((η ≫ 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))
have 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))
Tactic: simp only [comp_whiskerRight, tensorHom_def, Category.assoc,
      hom_inv_whiskerRight_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mon (goal)
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) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X)
    (X ◁ (η ≫ e.hom) ≫ (e.inv ⊗ₘ e.inv) ≫ μ ≫ e.hom) (Iso.hom (ρ_ X))
have 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))
Tactic: rw [← cancel_epi (ρ_ X).inv]