no goals
k : Type u₁
G : Type u₂
R : Type ?u.478651
inst✝² : Semiring k
inst✝¹ : MulOneClass G
inst✝ : Nontrivial k
a b : G
h : ↑(of k G) a = ↑(of k G) b
⊢ a = b
simpa using (single_eq_single_iff _ _ _ _).mp h