no goals
k : Type u₁
G : Type u₂
R✝ : Type ?u.870217
R : Type u_1
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Semiring R
f g : MonoidAlgebra k G →+* R
h₁ : ∀ (b : k), ↑f (single 1 b) = ↑g (single 1 b)
h_of : ∀ (a : G), ↑f (single a 1) = ↑g (single a 1)
a : G
b : k
⊢ ↑((fun f => ↑f) f) (Finsupp.single a b) = ↑((fun f => ↑f) g) (Finsupp.single a b)
rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single, AddMonoidHom.coe_coe f,
  AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]