no goals
k : Type u₁
G : Type u₂
R : Type ?u.2737055
inst✝⁵ : CommSemiring k
inst✝⁴ : AddMonoid G
A : Type u₃
inst✝³ : Semiring A
inst✝² : Algebra k A
B : Type ?u.2737092
inst✝¹ : Semiring B
inst✝ : Algebra k B
F : AddMonoidAlgebra k G →ₐ[k] A
f : MonoidAlgebra k G
⊢ ↑F f = sum f fun a b => b • ↑F (single a 1)
conv_lhs =>
  rw [lift_unique' F]
  simp [lift_apply]