-- Mathlib/RepresentationTheory/Basic.lean
theorem ofModule_asAlgebraHom_apply_apply (r : MonoidAlgebra k G)
    (m : RestrictScalars k (MonoidAlgebra k G) M) :
    ((ofModule M).asAlgebraHom r) m =
      (RestrictScalars.addEquiv _ _ _).symm (r • RestrictScalars.addEquiv _ _ _ m)

Proof state:
case hadd
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
f g : MonoidAlgebra k G
fw :
  ((ofModule M).asAlgebraHom f) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
gw :
  ((ofModule M).asAlgebraHom g) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ((ofModule M).asAlgebraHom (f + g)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((f + g) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]

Result:
no goals

Proof state:
case hM
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (g : G),
    ((ofModule M).asAlgebraHom ((of k G) g)) m =
      (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
        ((of k G) g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
intro g

Result:
case hM
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
g : G
⊢ ((ofModule M).asAlgebraHom ((of k G) g)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((of k G) g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Proof state:
case hsmul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r✝ : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
r : k
f : MonoidAlgebra k G
w :
  ((ofModule M).asAlgebraHom f) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ((ofModule M).asAlgebraHom (r • f)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((r • f) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
simp only [w, map_smul, LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul]

Result:
no goals

Proof state:
case hM
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
g : G
⊢ ((ofModule M).asAlgebraHom ((of k G) g)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((of k G) g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
simp only [one_smul, MonoidAlgebra.lift_symm_apply, MonoidAlgebra.of_apply,
  Representation.asAlgebraHom_single, Representation.ofModule, AddEquiv.apply_eq_iff_eq,
  RestrictScalars.lsmul_apply_apply]

Result:
no goals

Proof state:
case hadd
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (f g : MonoidAlgebra k G),
    ((ofModule M).asAlgebraHom f) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ((ofModule M).asAlgebraHom g) m =
          (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
            (g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
        ((ofModule M).asAlgebraHom (f + g)) m =
          (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
            ((f + g) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
intro f g fw gw

Result:
case hadd
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
f g : MonoidAlgebra k G
fw :
  ((ofModule M).asAlgebraHom f) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
gw :
  ((ofModule M).asAlgebraHom g) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (g • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ((ofModule M).asAlgebraHom (f + g)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((f + g) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Proof state:
case hsmul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (r : k) (f : MonoidAlgebra k G),
    ((ofModule M).asAlgebraHom f) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ((ofModule M).asAlgebraHom (r • f)) m =
        (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
          ((r • f) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

Tactic:
intro r f w

Result:
case hsmul
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Monoid G
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r✝ : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
r : k
f : MonoidAlgebra k G
w :
  ((ofModule M).asAlgebraHom f) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (f • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ((ofModule M).asAlgebraHom (r • f)) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm
      ((r • f) • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)