k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type ?u.351323
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) (↑(↑(ofModule (asModule ρ)) g) x) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm
            (RestrictScalars.addEquiv k (MonoidAlgebra k G)
              ((fun x => asModule ρ)
                (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type ?u.351323
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(↑(ofModule (asModule ρ)) g) x =
    ↑(AddEquiv.symm
          (RestrictScalars.addEquiv k (MonoidAlgebra k G)
            ((fun x => asModule ρ)
              (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))))
      (↑(AddEquiv.symm (asModuleEquiv ρ))
        (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))
apply_fun RestrictScalars.addEquiv _ _ ρ.asModule using
  (RestrictScalars.addEquiv _ _ ρ.asModule).injective
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type ?u.351323
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (MonoidAlgebra.single g 1 • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type ?u.351323
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) (↑(↑(ofModule (asModule ρ)) g) x) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm
            (RestrictScalars.addEquiv k (MonoidAlgebra k G)
              ((fun x => asModule ρ)
                (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
dsimp [ofModule, RestrictScalars.lsmul_apply_apply]
no goals
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type ?u.351323
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (MonoidAlgebra.single g 1 • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
simp