Zulip Chat Archive

Stream: new members

Topic: M40001 term sheet 2


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 23:01):

There's a tactic which does this I think

view this post on Zulip 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

view this post on Zulip Jalex Stark (Dec 09 2019 at 23:26):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 23:27):

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

view this post on Zulip Jalex Stark (Dec 09 2019 at 23:27):

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


Last updated: May 15 2021 at 23:13 UTC