# Zulip Chat Archive

## Stream: new members

### Topic: Inequalities with Reals

#### ROCKY KAMEN-RUBIO (Apr 25 2020 at 01:34):

I'm trying to prove `¬ real.sqrt 5 = 0`

. I know that for `nat`

s we would just do `cc`

, but tactics like `ring`

don't seem to be working for me here. I'm also having trouble finding theorems in mathlib that relate to inequalities with reals, or theorems from other typeclasses that are inherited by the reals. I'm could transform this into expressions like `¬ 5 = 0`

using `(0:ℝ) ≤ (5:ℝ)`

and `real.sqrt_eq_zero`

, but then I run into the same issue. Could someone point me in the right direction?

#### Reid Barton (Apr 25 2020 at 01:35):

The `norm_num`

tactic will prove `¬ 5 = 0`

, at least.

#### Shing Tak Lam (Apr 25 2020 at 01:38):

In fact `norm_num`

could prove your initial goal.

import tactic data.real.basic example : ¬ real.sqrt 5 = 0 := by norm_num

#### Mario Carneiro (Apr 25 2020 at 01:42):

this is almost certainly one of those times when it's not `norm_num`

doing the work

#### Reid Barton (Apr 25 2020 at 01:43):

`@[simp] theorem sqrt_eq_zero (h : 0 ≤ x) : sqrt x = 0 ↔ x = 0`

#### Mario Carneiro (Apr 25 2020 at 01:45):

aha:

example : ¬ real.sqrt 5 = 0 := by simp [ show 0 ≤ (5:ℝ), by norm_num, show (5:ℝ) ≠ 0, by norm_num]

#### Mario Carneiro (Apr 25 2020 at 01:45):

it's because `norm_num`

calls `simp`

with `norm_num`

as discharger

#### ROCKY KAMEN-RUBIO (Apr 25 2020 at 20:37):

Somewhat related inequality question: I'm trying to do this pretty simple limit proof. I get this far, and I know conceptually I need to use `he`

and the inverse of `hn`

to finesse my goal state into something trivial, but I can't seem to get there with the theorems I know (especially with the type casting). Could someone point me in the right direction?

import data.real.basic import data.nat.basic import algebra.archimedean def lim_to_inf (x : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε example : lim_to_inf (λ n, 1/n) 0 := begin rw lim_to_inf, intro ε, intro hε, have he := exists_nat_gt ε, cases he with N he, use N, intro n, intro hn, simp, end

#### Kevin Buzzard (Apr 25 2020 at 20:54):

What if epsilon=0.1, N=1, and n=1? Then the goal is false.

#### Chris Hughes (Apr 25 2020 at 21:01):

You want a `nat`

greater than `1/epsilon`

I think.

#### Kevin Buzzard (Apr 25 2020 at 21:43):

I would write down a careful paper proof first, and then think about how to get each line into Lean.

Last updated: May 13 2021 at 21:12 UTC