k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
this :
  AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
⊢ ↑(liftNC ↑f ↑g) (c • φ) = ↑f c * ↑(liftNC ↑f ↑g) φ

case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ ↑(liftNC ↑f ↑g) (c • φ) = ↑f c * ↑(liftNC ↑f ↑g) φ
suffices :
  (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) =
    (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g)
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
this :
  AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
⊢ ↑(liftNC ↑f ↑g) (c • φ) = ↑f c * ↑(liftNC ↑f ↑g) φ

case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
exact FunLike.congr_fun this φ
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c)) (singleAddHom a)) b =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)) (singleAddHom a)) b
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c) =
    AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)
refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (G →₀ k)) c)) (singleAddHom a)) b =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)) (singleAddHom a)) b
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (MonoidAlgebra k G)) c)) (singleAddHom a)) b =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)) (singleAddHom a)) b
unfold MonoidAlgebra
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(liftNC ↑f ↑g) (Finsupp.single a (c * b)) = ↑f c * ↑(liftNC ↑f ↑g) (Finsupp.single a b)
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.comp (liftNC ↑f ↑g) (↑(smulAddHom k (G →₀ k)) c)) (singleAddHom a)) b =
    ↑(AddMonoidHom.comp (AddMonoidHom.comp (AddMonoidHom.mulLeft (↑f c)) (liftNC ↑f ↑g)) (singleAddHom a)) b
simp
no goals
case this
k : Type u₁
G : Type u₂
R✝ : Type ?u.528207
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_1
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
a : G
b : k
⊢ ↑(liftNC ↑f ↑g) (Finsupp.single a (c * b)) = ↑f c * ↑(liftNC ↑f ↑g) (Finsupp.single a b)
rw [liftNC_single, liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]