M40001 term sheet 2

Stream: new members

[Jalex Stark]

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]

There's a tactic which does this I think

[Kevin Buzzard]

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

[Jalex Stark]

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

[Kevin Buzzard]

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]

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

[Jalex Stark]

is assumption kind of like exact _?
edit: answer, yes, see https://leanprover.github.io/reference/tactics.html