feat(nat/basic): more nat.find lemmas (#6002)

also merge two sections on nat.find

src/data/nat/basic.lean

@@ -1257,23 +1257,38 @@ end
 /-! ### `find` -/
 section find
 
-lemma find_eq_iff {p : ℕ → Prop} [decidable_pred p] (h : ∃ n, p n) {m} :
-  nat.find h = m ↔ p m ∧ ∀ n < m, ¬ p n :=
+variables  {p q : ℕ → Prop} [decidable_pred p] [decidable_pred q]
+
+lemma find_eq_iff (h : ∃ n : ℕ, p n) : nat.find h = m ↔ p m ∧ ∀ n < m, ¬ p n :=
 begin
   split,
   { rintro rfl, exact ⟨nat.find_spec h, λ _, nat.find_min h⟩ },
   { rintro ⟨hm, hlt⟩,
     exact le_antisymm (nat.find_min' h hm) (not_lt.1 $ imp_not_comm.1 (hlt _) $ nat.find_spec h) }
 end
 
-@[simp] lemma find_eq_zero {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
-  nat.find h = 0 ↔ p 0 :=
+@[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]
+
+@[simp] lemma find_eq_zero (h : ∃ n : ℕ, p n) : nat.find h = 0 ↔ p 0 :=
 by simp [find_eq_iff]
 
-@[simp] lemma find_pos {p : ℕ → Prop} [decidable_pred p] (h : ∃ (n : ℕ), p n) :
-  0 < nat.find h ↔ ¬ p 0 :=
+@[simp] lemma find_pos (h : ∃ n : ℕ, p n) : 0 < nat.find h ↔ ¬ p 0 :=
 by rw [pos_iff_ne_zero, not_iff_not, nat.find_eq_zero]
 
+theorem find_le (h : ∀ n, q n → p n) (hp : ∃ n, p n) (hq : ∃ n, q n) :
+  nat.find hp ≤ nat.find hq :=
+nat.find_min' _ ((h _) (nat.find_spec hq))
+
 end find
 
 /-! ### `find_greatest` -/
@@ -1605,11 +1620,4 @@ instance decidable_exists_lt {P : ℕ → Prop} [h : decidable_pred P] :
 | (n + 1) := decidable_of_decidable_of_iff (@or.decidable _ _ (decidable_exists_lt n) (h n))
   (by simp only [lt_succ_iff_lt_or_eq, or_and_distrib_right, exists_or_distrib, exists_eq_left])
 
-/-! ### find -/
-
-theorem find_le {p q : ℕ → Prop} [decidable_pred p] [decidable_pred q]
-  (h : ∀ n, q n → p n) (hp : ∃ n, p n) (hq : ∃ n, q n) :
-  nat.find hp ≤ nat.find hq :=
-nat.find_min' _ ((h _) (nat.find_spec hq))
-
 end nat