nat.find_ge_of_not?

Stream: Is there code for X?

[Ryan Lahfa]

I'm looking for something like this:

import data.real.basic
import data.nat.choose.basic

lemma nat.const_le_find_of_not (p: ℕ → Prop) [decidable_pred p] (c: ℕ) (H: ∃ n, p n):
  (∀ (n: ℕ), n ≤ c → ¬ p n) → c ≤ nat.find H := sorry

theorem mwe (exists_nat_unbdd: ∃ z : ℕ, abs (z: ℝ) > 1):
  2 ≤ nat.find exists_nat_unbdd := sorry

It appears to me it does not exist in mathlib, should this exist? In this case, I believe I could finish the main theorem by some decidability tactic, am I wrong?

[Floris van Doorn]

The first inequality is an easy consequence of docs#nat.find_spec (by contradiction).
You can even make one of the \le into <. Is it worth adding? Not sure.

[Floris van Doorn]

I think the first lemma (and variants) is useful when formulated as iff:

@[simp] lemma find_lt_iff (h : ∃ n : ℕ, p n) (n : ℕ) : nat.find h < n ↔ ∃ m < n, p m :=
⟨λ h2, ⟨nat.find h, h2, nat.find_spec h⟩, λ ⟨m, hmn, hm⟩, (nat.find_min' h hm).trans_lt hmn⟩

@[simp] lemma find_le_iff (h : ∃ n : ℕ, p n) (n : ℕ) : nat.find h ≤ n ↔ ∃ m ≤ n, p m :=
by simp only [exists_prop, ← lt_succ_iff, find_lt_iff]

@[simp] lemma le_find_iff (h : ∃ (n : ℕ), p n) (n : ℕ) : n ≤ nat.find h ↔ ∀ m < n, ¬ p m :=
by simp_rw [← not_lt, not_iff_comm, not_forall, not_not, find_lt_iff]

@[simp] lemma lt_find_iff (h : ∃ n : ℕ, p n) (n : ℕ) : n < nat.find h ↔ ∀ m ≤ n, ¬ p m :=
by simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]

See #6002

[Ryan Lahfa]

Really, thanks a lot!

[Ryan Lahfa]

Indeed, I had the feeling they were not that far from find_spec or find_min, but it's really cool they are in mathlib now :)