Uniform way of saying there is a coercion to Real?

Stream: mathlib4

[Michael Stoll]

Is there a way to fill in the ? below

import Mathlib

lemma Complex.cast_ofReal {α : Type*} [?] (a : α) : (a : ℂ) = (a : ℝ) := sorry

so that for n : ℕ, Complex.cast_of_Real n is syntactically the same as Complex.nat_cast_ofReal, where

lemma Complex.nat_cast_ofReal (a : ℕ) : (a : ℂ) = (a : ℝ) := rfl

(and similarly for Int and Rat...) ?

I tried [Coe α ℝ], which results in a rfl lemma, but does not trigger when applied to n : ℕ since there is no [Coe ℕ ℝ] instance. There seem to be type classes for coercions from Nat (or Int or Rat...): docs#NatCast, docs#IntCast, docs#RatCast, but what I need here is a type class for coercions to Real.

For motivation/background, see here.

[Michael Stoll]

I see that there are docs#Complex.ofReal_nat_cast, docs#Complex.ofReal_int_cast, docs#Complex.ofReal_rat_cast. The fact that there are separate lemmas for each of these likely indicates that there is no way of stating this so that it applies to all of them.

[Yaël Dillies]

Yep, exactly. You should write one for each.

[Michael Stoll]

What is the rationale behind setting it up in this way? I assume using the analogue of Coe in Lean3 would have worked.

[Eric Wieser]

The design of Coe in lean 4 means you should pretty much never write [Coe A B], as then your lemma ends up about Coe.coe, but any real use will be about A.toB (as ↑ unfolds the Coe.coe as part of elaboration)

[Eric Wieser]

This is a great change from Lean 3 because it makes the goal easier to understand as you no longer have coe mean lots of different things, but is also a terrible change because it makes general lemmas harder to write as you no longer have coe mean lots of different things.