How to convert the 2:N to 2:R in proof?

Stream: new members

[Colin Jones ⚛️]

I have this problem:

import Mathlib.Data.Real.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.FieldTheory.Perfect

variable {x y z : ℝ}
example (h : x ≠ 0) (hy : y ≥ 0) : 2*x = x*y^2 → y = Real.sqrt 2 := by
  intro h1
  rw [mul_comm x, ← div_left_inj' h, mul_div_assoc, mul_div_assoc] at h1
  rw [show x/x = 1 by apply div_self h, mul_one, mul_one] at h1
  have h1' := by apply Eq.symm h1
  have h2 : 2 = ((2:ℝ) ^ ((1:ℝ)/(2:ℝ) * 2)) := by norm_num
  rw [Real.sqrt_eq_rpow]; nth_rw 1 [h2, h1]; norm_num
  apply Eq.symm
  calc
    (y ^ 2) ^ (1 / 2) = y ^ (2 * (1/2)) := by rw [← Real.rpow_mul hy]
    _ = y := by norm_num

The error in the goal statement looks like:
Screenshot-2023-11-08-170853.png

The difference I found out was the first 2 is a natural number but the calc block uses a real number 2 instead. How do I convert?

[Alex J. Best]

There are ways to convert, but they will not work in this case as the natural number 1/2 is actually 0 (division of the natural numbers is defined to be floor division) so instead you should try to never introduce 1/2 as a natural number in the first place. You can use a type ascription like (y ^ 2) ^ (1 / 2 : ℝ) to force the meaning you want, but the proof you have written there in the calc block wont work any more without changes

[Eric Wieser]

Is this lean4#2220 again?

[Colin Jones ⚛️]

It’s not the 1/2 that’s the issue. It’s the first number 2 in y^2 that’s causing the discrepancy.

[Colin Jones ⚛️]

Eric Wieser said:

Is this lean4#2220 again?

Is it a bug?

[Colin Jones ⚛️]

Can anyone offer a way to fix this?

[Ruben Van de Velde]

Have you tried adding

macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y)

to the top of your file?

[Kyle Miller]

Colin, this is a workaround for a Lean 4 issue that's been already fixed. We're working on updating mathlib to the newest version of Lean 4 at the moment, so it shouldn't be necessary soon.

[Kyle Miller]

This workaround makes it so you can reliably control whether you're getting the ^ with a Nat exponent or a Real exponent by inserting type ascriptions.