feat: f r = r for f : ℝ →+* ℝ (leanprover-community#30486)

Author: vihdzp

Mathlib/Data/Real/CompleteField.lean

@@ -18,3 +18,8 @@ instance Real.RingHom.unique : Unique (ℝ →+* ℝ) where
   default := RingHom.id ℝ
   uniq f := congr_arg OrderRingHom.toRingHom (@Subsingleton.elim (ℝ →+*o ℝ) _
       ⟨f, ringHom_monotone (fun r hr => ⟨√r, sq_sqrt hr⟩) f⟩ default)
+
+@[simp]
+theorem Real.ringHom_apply {F : Type*} [FunLike F ℝ ℝ] [RingHomClass F ℝ ℝ] (f : F) (r : ℝ) :
+    f r = r :=
+  DFunLike.congr_fun (Unique.eq_default (RingHomClass.toRingHom f)) r