Limit inequality

Stream: new members

[Pedro Minicz]

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]

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]

contrapose! makes it so much easier! Thank you!

[Pedro Minicz]

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]

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]

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]

I think you are thinking of specialize

[Pedro Minicz]

Oh, I was thinking of revert.

[Pedro Minicz]

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

[Mario Carneiro]

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

[Mario Carneiro]

I don't think you can revert an expression

[Pedro Minicz]

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]

Mario Carneiro said:

I don't think you can revert an expression

What exactly you mean by expression?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Pedro Minicz]

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: