no goals
k : Type u₁
G : Type u₂
R : Type ?u.2579273
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2579310
inst✝¹ : Semiring B
inst✝ : Algebra k B
F : Multiplicative G →* A
f : MonoidAlgebra k G
⊢ ↑(↑(lift k G A) F) f = sum f fun a b => b • ↑F (↑Multiplicative.ofAdd a)
simp only [lift_apply', Algebra.smul_def]