Dealing with Coercing Real to Complex

Stream: new members

[Gregory Wickham]

In the course of a much larger proof, I want to show

import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
import Mathlib.Data.Complex.Basic

noncomputable def c : ℝ := 1 + (2:ℝ) ^ ((1:ℝ)/(2:ℝ))
example : (c : ℂ) = 1 + ↑((2:ℝ) ^ ((1:ℝ)/(2:ℝ))) := by sorry

It seems like it should be trivial, but I just can't figure out how to do it. I needed to declare the original constant to be real to prove certain properties of it, but alternatively, if there is a way to declare it complex initially and then prove that it is its own conjugate and has 0 imaginary part, that would probably work too. How can I fix this issue?

[Ruben Van de Velde]

by norm_cast solves it

[Gregory Wickham]

You're right. In this example, it works, but in the original context, it doesn't. It seems I haven't recreated the issue correctly. I will try to construct a better minimal example