awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
⊢ Eq (α := S[M] →+ R)
    (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
      ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
have hfg : ∀ (m : M) (x : S),
  Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
      ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
          ((singleAddHom m : (a : S) → S[M]) x) :
        S[M]) :
    R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₁ : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
      ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
    R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₂ : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) : R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) : R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₃ : (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
  HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) : R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₃ :
  (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₄ : (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m (c * x)) =
  HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) : R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₃ :
  (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
hfg₄ :
  (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m (c * x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₅ : HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) (c * x) : R) ((g : (a : M) → R) m : R) =
  HMul.hMul (α := R) ((f : (a : S) → R) c : R)
    (HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) x : R) ((g : (a : M) → R) m : R))
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) ((singleAddHom m : (a : S) → S[M]) x : S[M]) : R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) : R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₃ :
  (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
hfg₄ :
  (liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m (c * x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : M) → R) : (a : S[M]) → R) (single m x) : R)
hfg₅ :
  HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) (c * x) : R) ((g : (a : M) → R) m : R) =
    HMul.hMul (α := R) ((f : (a : S) → R) c : R)
      (HMul.hMul (α := R) (β := R) (((↑f : S →+ R) : (a : S) → R) x : R) ((g : (a : M) → R) m : R))
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c)) (liftNC (↑f : S →+ R) (⇑g : (a : M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₆ : HMul.hMul (α := R) (β := R) ((f : (a : S) → R) (c * x) : R) ((g : (a : M) → R) m : R) =
  HMul.hMul (α := R) ((f : (a : S) → R) c : R)
    (HMul.hMul (α := R) (β := R) ((f : (a : S) → R) x : R) ((g : (a : M) → R) m : R))
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : IsScalarTower R k k
t : R
a b : k[G]
⊢ (t • a) • b = t • a • b
have hfg : ∀ (m : G), Eq.{u₁ + 1} (α := k) (((t • a) • b : (a : G) → k) m : k) ((t • a • b : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : IsScalarTower R k k
t : R
a b : k[G]
⊢ (t • a) • b = t • a • b
have hfg : ∀ (m : G), Eq.{u₁ + 1} (α := k) (((t • a) • b : (a : G) → k) m : k) ((t • a • b : (a : G) → k) m : k)
Tactic: classical ext; simp [mul_apply, sum_smul_index' (b := t), smul_sum, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
⊢ t • a • b = a • t • b
have hfg : ∀ (m : G), Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)
have hfg : Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
  (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
Tactic: simp only [smul_eq_mul, mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
    (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
have hfg : HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
  sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
Tactic: rw [coe_smul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
have hfg : ∀ (a₁ : G) (b₁ : k) (i : G), (if a₁ * i = m then b₁ * 0 else 0) = 0
Tactic: refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg : ∀ (a₁ : G) (b₁ : k) (i : G), (if a₁ * i = m then b₁ * 0 else 0) = 0
⊢ HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
have hfg₁ : (sum a fun (a₁ : G) (b₁ : k) ↦ sum b fun (i : G) (c : k) ↦ if a₁ * i = m then b₁ * t • c else 0) =
  HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m
Tactic: refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)
have hfg : Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
  (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
Tactic: classical
    simp only [smul_eq_mul, mul_apply]
    rw [coe_smul]
    refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
    simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg :
  Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
    (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
⊢ Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)
have hfg₁ : HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
  sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
Tactic: classical
    simp only [smul_eq_mul, mul_apply]
    rw [coe_smul]
    refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
    simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
⊢ f • v ∈ (↑W : Set V)
have rw : ∑ i ∈ f.support, HSMul.hSMul (α := k[G]) (Finsupp.single i ((f : (a : G) → k) i) : G →₀ k) v ∈ (↑W : Set V)
Tactic: rw [← Finsupp.sum_single f, Finsupp.sum, Finset.sum_smul]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ i ∈ f.support, HSMul.hSMul (α := k[G]) (Finsupp.single i ((f : (a : G) → k) i) : G →₀ k) v ∈ (↑W : Set V)
have simp_rw : ∑ x ∈ f.support,
    HSMul.hSMul.{u₁, u_5, u_5} (α := k) ((f : (a : G) → k) x : k)
      (HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) x : k[G]) v) ∈
  (↑W : Set V)
Tactic: simp_rw [← smul_of, smul_assoc]