## Stream: new members

### Topic: M40001 term sheet 2

#### Jalex Stark (Dec 09 2019 at 22:51):

How do I look for the fact "the inclusion \N \r \R is a homomorphism of ordered rings"? In particular I am trying to kill the following tactic state
x : ℝ,
hx_w : ℤ,
hx_h : x = ↑hx_w ∧ x ^ 2 < 3
⊢ 3 > hx_w ^ 2

#### Kevin Buzzard (Dec 09 2019 at 23:01):

There's a tactic which does this I think

#### Kevin Buzzard (Dec 09 2019 at 23:02):

You could split hx_h into h1 and h2, and then do cases on h1 and then try norm_cast

#### Jalex Stark (Dec 09 2019 at 23:26):

These exercises really make one feel like one is learning math for the first time :)

#### Kevin Buzzard (Dec 09 2019 at 23:26):

import data.real.basic

example (x : ℝ) (hx_w : ℤ)
(hx_h : x = ↑hx_w ∧ x ^ 2 < 3) :
3 > hx_w ^ 2 :=
begin
cases hx_h with h1 h2,
rw h1 at h2,
norm_cast at h2,
assumption,
end


#### Kevin Buzzard (Dec 09 2019 at 23:27):

yeah, this stuff really opened my eyes and I was the teacher at the time.

#### Jalex Stark (Dec 09 2019 at 23:27):

is assumption kind of like exact _?