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
M : C
inst_2 : MonObj M
X : C
h₂ : ModObj M X
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
H :
  Eq.{v₁ + 1} (α :=
    @MonoidalLeftActionStruct.actionObj.{v₁, u₁, v₁, u₁} _ _ inst inst toMonoidalCategoryStruct _ M X ⟶ X)
    (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _) (@ModObj.smul _ _ _ _ _ _ _ inst_2 _ _)
⊢ { smul := smul, one_smul := one_smul, mul_smul := mul_smul : ModObj M X } = h₂
have mk : ∀ (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 _ _)),
  { 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: cases h₂
Cleared hypotheses: h₂, H
-- 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
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 _ _)
⊢ { 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 }
have 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 }
Tactic: subst H
Cleared hypotheses: smul_1, one_smul_1, mul_smul_1, H
-- 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 : 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)
have 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)
Tactic: rw [actionHom_def', comp_actionHomLeft, action_exchange_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 : 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)
⊢ 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)
have 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)
Tactic: rw [actionHom_def', comp_actionHomLeft, action_exchange_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 : 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)
⊢ 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)
have 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)
Tactic: rw [actionHom_def', comp_actionHomLeft, action_exchange_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (hypothesis)
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 ⟶ Y)
    (η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) ≫ @smul _ _ _ _ _ _ _ inst_4 _ _ ≫ e₂.hom) (Iso.hom (λₗ Y))
have 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)
Tactic: have : η ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = _ ⊴ₗ e₂.inv ≫ (η ≫ e₁.inv) ⊵ₗ X := by
      rw [actionHom_def', comp_actionHomLeft, action_exchange_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 : 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)
have 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)
Tactic: rw [actionHom_def', action_exchange, ← comp_actionHomLeft_assoc, IsMonHom.mul_hom,
        comp_actionHomLeft, Category.assoc, ← action_exchange, actionHom_def']
-- 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 : 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)
    ((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)
have 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)
Tactic: nth_rw 2 [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 : 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)
    ((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)
have 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)
Tactic: rw [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (hypothesis)
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 ⟶ 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)
have 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)
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]
-- 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 : 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 (α :=
    @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)
have 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)
Tactic: rw [reassoc_of% this]
-- 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 : 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)
have 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)
Tactic: rw [← actionHomLeft_action_assoc, 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 : 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)
⊢ 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)
have 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 _ _)
Tactic: rw [← actionHomLeft_action_assoc, action_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Mod (hypothesis)
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 (α :=
    @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)
have 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)
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]
-- 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 _ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) M ⟶ M)
    (η ⊵ₗ M ≫ f ⊵ₗ M ≫ @ModObj.smul _ _ _ _ _ _ _ inst_10 _ _) (Iso.hom (λₗ M))
have 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))
Tactic: rw [← comp_actionHomLeft_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
⊢ 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))
have 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))
Tactic: rw [IsMonHom.one_hom, ModObj.one_smul]
-- 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 _ (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))
⊢ 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))
have 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))
Tactic: rw [IsMonHom.one_hom, ModObj.one_smul]