coercions between real and nat

Stream: new members

[Julia Ramos Alves]

Hello there, I'm new at using Lean and I have a rather simple problem that I haven't yet been able to find a solution for. I'm trying to write an equality of real numbers but the terms for the left hand side are causing it to be interpreted as a natural number. How do I coerce it? I'm using division for it, is there some kind of "real division" I should be using instead?

[David Renshaw]

you can coerce like this: (x : ℝ)

[David Renshaw]

try doing that on some of the innermost terms

[Julia Ramos Alves]

the only variable that I had was just a sum index, so it had to be natural, but it seems like using "coe" works

[Kevin Buzzard]

@Julia Ramos Alves for reference: the best way to ask questions here is to post working code with all imports etc in it, so that other people can just cut and paste into VS Code and see the same problem as you. You'll then learn quickly that people usually give very efficient answers on this forum. See #mwe (that's a link) for more details on this technique.