## Stream: new members

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

#### Colin Jones ⚛️ (Nov 08 2023 at 22:16):

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 (Nov 08 2023 at 22:44):

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 (Nov 08 2023 at 23:12):

Is this lean4#2220 again?

#### Colin Jones ⚛️ (Nov 08 2023 at 23:15):

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 ⚛️ (Nov 08 2023 at 23:16):

Eric Wieser said:

Is this lean4#2220 again?

Is it a bug?

#### Colin Jones ⚛️ (Nov 13 2023 at 22:34):

Can anyone offer a way to fix this?

#### Ruben Van de Velde (Nov 13 2023 at 22:59):

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


to the top of your file?

#### Kyle Miller (Nov 13 2023 at 23:01):

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 (Nov 13 2023 at 23:02):

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.

Last updated: Dec 20 2023 at 11:08 UTC