case hM
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (g : G),
    ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
      ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
        (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

case hadd
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (f g : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) g) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
        ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

case hsmul
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (r : k) (f : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ↑(↑(asAlgebraHom (ofModule M)) r) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
apply MonoidAlgebra.induction_on r
case hM
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
g : G
⊢ ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
case hM
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (g : G),
    ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
      ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
        (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
intro g
no goals
case hM
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
g : G
⊢ ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
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]
case hadd
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
f g : MonoidAlgebra k G
fw :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
gw :
  ↑(↑(asAlgebraHom (ofModule M)) g) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
case hadd
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (f g : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) g) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
        ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
intro f g fw gw
no goals
case hadd
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
f g : MonoidAlgebra k G
fw :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
gw :
  ↑(↑(asAlgebraHom (ofModule M)) g) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]
case hsmul
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
r : k
f : MonoidAlgebra k G
w :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
case hsmul
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (r : k) (f : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
intro r f w
no goals
case hsmul
k : Type u_1
G : Type u_2
V : Type ?u.309923
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 : RestrictScalars k (MonoidAlgebra k G) M
r : k
f : MonoidAlgebra k G
w :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
simp only [w, AlgHom.map_smul, LinearMap.smul_apply,
  RestrictScalars.addEquiv_symm_map_smul_smul]