-- Mathlib/RepresentationTheory/Basic.lean
theorem ofModule_asModule_act (g : G) (x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule) :
    ofModule (k := k) (G := G) ρ.asModule g x = -- Porting note: more help with implicit
      (RestrictScalars.addEquiv _ _ _).symm
        (ρ.asModuleEquiv.symm (ρ g (ρ.asModuleEquiv (RestrictScalars.addEquiv _ _ _ x))))

Proof state:
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
g : G
x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (MonoidAlgebra.single g 1 • (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)) =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (ρ.asModuleEquiv.symm
          ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))

Tactic:
simp

Result:
no goals

Proof state:
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
g : G
x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule
⊢ ((ofModule ρ.asModule) g) x =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x))))

Tactic:
apply_fun RestrictScalars.addEquiv _ _ ρ.asModule using
  (RestrictScalars.addEquiv _ _ ρ.asModule).injective

Result:
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
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)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (ρ.asModuleEquiv.symm
          ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))

Proof state:
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
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)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (ρ.asModuleEquiv.symm
          ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))

Tactic:
dsimp [ofModule, RestrictScalars.lsmul_apply_apply]

Result:
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
g : G
x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule
⊢ (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (MonoidAlgebra.single g 1 • (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)) =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule)
      ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
        (ρ.asModuleEquiv.symm
          ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))