no goals
E : Type ?u.1071891
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ →+* ℂ
h : Continuous ↑f
⊢ f = ofReal
convert congr_arg AlgHom.toRingHom <| Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h)
  (Algebra.ofId ℝ ℂ)