## Stream: new members

### Topic: Casting Problem

#### Dan Stanescu (Jun 04 2020 at 13:43):

This example may be a little more verbose than needed, but is there a way to solve it?

import data.real.basic

example (N : ℕ) (a : ℝ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:ℝ)/ a ) ) :
0 < N :=
begin
have H1 := lt_of_lt_of_le ha (le_nat_ceil ( (1:ℝ)/a )),
rw ← hN at H1,
have H2 : N = ↑N, norm_cast, rw H2,
exact H1, -- fails
end


#### Jalex Stark (Jun 04 2020 at 13:44):

i haven't tried your code yet because I"m not at a computer, but I bet things will be easier for you if you use integers instead of naturals

#### Jalex Stark (Jun 04 2020 at 13:46):

I don't think H2 means what you want it to mean

#### Dan Stanescu (Jun 04 2020 at 13:47):

Yes but I just can't in this example. It's part of a bigger proof. I can bet you're right about H2.

#### Jalex Stark (Jun 04 2020 at 13:51):

this works

example (N : ℕ) (a : ℝ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:ℝ)/ a ) ) :
0 < N :=
begin
have H1 := lt_of_lt_of_le ha (le_nat_ceil ( (1:ℝ)/a )),
rw ← hN at H1,
revert H1, norm_cast,
exact id
end


#### Jalex Stark (Jun 04 2020 at 13:52):

the only way I know to get norm_cast to do what i want is to put all the information it needs into the goal state

#### Jalex Stark (Jun 04 2020 at 13:55):

actually in this case norm_cast at H1 does fine

#### Jalex Stark (Jun 04 2020 at 13:56):

example (N : ℕ) (a : ℝ) (ha: 0 < 1/a) (hN : N = nat_ceil ( (1:ℝ)/ a ) ) :
0 < N :=
begin
have := lt_of_lt_of_le ha (le_nat_ceil ( (1:ℝ)/a )),
norm_cast at this, rwa hN,
end


#### Dan Stanescu (Jun 04 2020 at 14:00):

And I thought I had exhausted all ways to ask norm_cast to do the job!

#### Dan Stanescu (Jun 04 2020 at 14:00):

Thanks @Jalex Stark !

#### Jalex Stark (Jun 04 2020 at 14:01):

Jalex Stark said:

the only way I know to get norm_cast to do what i want is to put all the information it needs into the goal state

actually it's push_cast that I get this headache with. I think norm_cast always tries to remove coercions

Last updated: May 13 2021 at 16:25 UTC