## Stream: new members

### Topic: Limit inequality

#### Pedro Minicz (Aug 14 2020 at 22:23):

I am having no luck proving the following example. I looked around mathlib and didn't seem to find anything that would directly help. How do I handle the universal qualified in the hypothesis (I mean, maybe transform the hypothesis into something more usable)? I feel like I am missing something here.

import data.real.basic

example {x : ℝ} (h : ∀ n : ℕ, x < (n + 1)⁻¹) : x ≤ 0 :=
sorry


#### Mario Carneiro (Aug 14 2020 at 22:28):

example {x : ℝ} : (∀ n : ℕ, x < (n + 1)⁻¹) → x ≤ 0 :=
begin
contrapose!,
intro h,
obtain ⟨n, h⟩ := exists_nat_one_div_lt h,
use n,
simpa using le_of_lt h
end


#### Pedro Minicz (Aug 14 2020 at 22:29):

contrapose! makes it so much easier! Thank you!

#### Pedro Minicz (Aug 14 2020 at 22:31):

By the way, there is a tactic similar to how generalize behaves in Coq. I remember seeing it a Lean/Coq cheatsheet but never managed to use it properly.

#### Mario Carneiro (Aug 14 2020 at 22:31):

alternatively:

example {x : ℝ} (h : ∀ n : ℕ, x < (n + 1)⁻¹) : x ≤ 0 :=
begin
refine le_of_not_gt (λ x0, _),
obtain ⟨n, h'⟩ := exists_nat_one_div_lt x0,
simp at h',
exact not_lt_of_lt (h _) h',
end


#### Mario Carneiro (Aug 14 2020 at 22:31):

example {x : ℝ} (h : ∀ n : ℕ, x < (n + 1)⁻¹) : x ≤ 0 :=
begin
refine le_of_not_gt (λ x0, _),
obtain ⟨n, h'⟩ := exists_nat_one_div_lt x0,
specialize h n,
simp at *, linarith
end


#### Mario Carneiro (Aug 14 2020 at 22:32):

I think you are thinking of specialize

#### Pedro Minicz (Aug 14 2020 at 22:32):

Oh, I was thinking of revert.

#### Pedro Minicz (Aug 14 2020 at 22:32):

https://github.com/jldodds/coq-lean-cheatsheet

#### Mario Carneiro (Aug 14 2020 at 22:33):

there is also a generalize, but it doesn't do the reverting part, only the find and replace

#### Mario Carneiro (Aug 14 2020 at 22:33):

I don't think you can revert an expression

#### Pedro Minicz (Aug 14 2020 at 22:33):

import data.real.basic

example {x : ℝ} (h : ∀ n : ℕ, x < (n + 1)⁻¹) : x ≤ 0 :=
begin
revert h,
contrapose!,
intro h,
obtain ⟨n, h⟩ := exists_nat_one_div_lt h,
use n,
simpa using le_of_lt h
end


#### Pedro Minicz (Aug 14 2020 at 22:34):

Mario Carneiro said:

I don't think you can revert an expression

What exactly you mean by expression?

#### Mario Carneiro (Aug 14 2020 at 22:34):

like you can't revert 2 + 2, you would have to generalize : 2 + 2 = x, revert x

#### Mario Carneiro (Aug 14 2020 at 22:35):

this would turn |- P (2+2) into |- \all x, P x

#### Mario Carneiro (Aug 14 2020 at 22:35):

I try to avoid intro and revert as the first line of a proof, as a matter of style

#### Mario Carneiro (Aug 14 2020 at 22:36):

you can almost always set up the theorem statement so that the appropriate things are already intro'd

#### Pedro Minicz (Aug 14 2020 at 22:37):

I see! Good example! I finally understand how generalize works. I tried and failed to use it several times because I was using like generalize is Coq. :grinning_face_with_smiling_eyes:

Last updated: May 11 2021 at 12:15 UTC