k : Type u_1
G : Type u_2
V : Type ?u.428533
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : asModule (ofModule M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M)
      (↑(↑(asAlgebraHom (ofModule M)) r) (↑(asModuleEquiv (ofModule M)) m)) =
    r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) m)
k : Type u_1
G : Type u_2
V : Type ?u.428533
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : asModule (ofModule M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) (r • m)) =
    r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) m)
dsimp
no goals
k : Type u_1
G : Type u_2
V : Type ?u.428533
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : asModule (ofModule M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M)
      (↑(↑(asAlgebraHom (ofModule M)) r) (↑(asModuleEquiv (ofModule M)) m)) =
    r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) m)
simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]