feat(data/nat/basic): Monotonicity of nat.find_greatest (#10507)

This proves that `nat.find_greatest` is monotone in both arguments.

src/data/nat/basic.lean

@@ -1270,19 +1270,22 @@ protected def find_greatest (P : ℕ → Prop) [decidable_pred P] : ℕ → ℕ
 | 0       := 0
 | (n + 1) := if P (n + 1) then n + 1 else find_greatest n
 
-variables {P : ℕ → Prop} [decidable_pred P]
+variables {P Q : ℕ → Prop} [decidable_pred P] {b : ℕ}
 
 @[simp] lemma find_greatest_zero : nat.find_greatest P 0 = 0 := rfl
 
-@[simp] lemma find_greatest_eq : ∀{b}, P b → nat.find_greatest P b = b
+lemma find_greatest_succ (n : ℕ) :
+  nat.find_greatest P (n + 1) = if P (n + 1) then n + 1 else nat.find_greatest P n := rfl
+
+@[simp] lemma find_greatest_eq : ∀ {b}, P b → nat.find_greatest P b = b
 | 0       h := rfl
 | (n + 1) h := by simp [nat.find_greatest, h]
 
-@[simp] lemma find_greatest_of_not {b} (h : ¬ P (b + 1)) :
+@[simp] lemma find_greatest_of_not (h : ¬ P (b + 1)) :
   nat.find_greatest P (b + 1) = nat.find_greatest P b :=
 by simp [nat.find_greatest, h]
 
-lemma find_greatest_eq_iff {b m} :
+lemma find_greatest_eq_iff :
   nat.find_greatest P b = m ↔ m ≤ b ∧ (m ≠ 0 → P m) ∧ (∀ ⦃n⦄, m < n → n ≤ b → ¬P n) :=
 begin
   induction b with b ihb generalizing m,
@@ -1293,10 +1296,10 @@ begin
   { by_cases hb : P (b + 1),
     { rw [find_greatest_eq hb], split,
       { rintro rfl,
-        exact ⟨le_refl _, λ _, hb, λ n hlt hle, (hlt.not_le hle).elim⟩ },
+        exact ⟨le_rfl, λ _, hb, λ n hlt hle, (hlt.not_le hle).elim⟩ },
       { rintros ⟨hle, h0, hm⟩,
         rcases decidable.eq_or_lt_of_le hle with rfl|hlt,
-        exacts [rfl, (hm hlt (le_refl _) hb).elim] } },
+        exacts [rfl, (hm hlt le_rfl hb).elim] } },
     { rw [find_greatest_of_not hb, ihb],
       split,
       { rintros ⟨hle, hP, hm⟩,
@@ -1309,30 +1312,51 @@ begin
         exact hb (hP b.succ_ne_zero) } } }
 end
 
-lemma find_greatest_eq_zero_iff {b} :
-  nat.find_greatest P b = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ b → ¬P n :=
+lemma find_greatest_eq_zero_iff : nat.find_greatest P b = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ b → ¬P n :=
 by simp [find_greatest_eq_iff]
 
-lemma find_greatest_spec {b} (h : ∃m, m ≤ b ∧ P m) : P (nat.find_greatest P b) :=
+lemma find_greatest_spec (hmb : m ≤ b) (hm : P m) : P (nat.find_greatest P b) :=
 begin
-  rcases h with ⟨m, hmb, hm⟩,
   by_cases h : nat.find_greatest P b = 0,
   { cases m, { rwa h },
     exact ((find_greatest_eq_zero_iff.1 h) m.zero_lt_succ hmb hm).elim },
   { exact (find_greatest_eq_iff.1 rfl).2.1 h }
 end
 
-lemma find_greatest_le {b} : nat.find_greatest P b ≤ b :=
-(find_greatest_eq_iff.1 rfl).1
+lemma find_greatest_le (n : ℕ) : nat.find_greatest P n ≤ n := (find_greatest_eq_iff.1 rfl).1
 
-lemma le_find_greatest {b m} (hmb : m ≤ b) (hm : P m) : m ≤ nat.find_greatest P b :=
+lemma le_find_greatest (hmb : m ≤ b) (hm : P m) : m ≤ nat.find_greatest P b :=
 le_of_not_lt $ λ hlt, (find_greatest_eq_iff.1 rfl).2.2 hlt hmb hm
 
-lemma find_greatest_is_greatest {b k} (hk : nat.find_greatest P b < k) (hkb : k ≤ b) :
-  ¬ P k :=
+lemma find_greatest_mono_right (P : ℕ → Prop) [decidable_pred P] : monotone (nat.find_greatest P) :=
+begin
+  refine monotone_nat_of_le_succ (λ n, _),
+  rw [find_greatest_succ],
+  split_ifs,
+  { exact (find_greatest_le n).trans (le_succ _) },
+  { refl }
+end
+
+lemma find_greatest_mono_left [decidable_pred Q] (hPQ : P ≤ Q) :
+  nat.find_greatest P ≤ nat.find_greatest Q :=
+begin
+  intro n,
+  induction n with n hn,
+  { refl },
+  by_cases P (n + 1),
+  { rw [find_greatest_eq h, find_greatest_eq (hPQ _ h)] },
+  { rw find_greatest_of_not h,
+    exact hn.trans (nat.find_greatest_mono_right _ $ le_succ _) }
+end
+
+lemma find_greatest_mono {a b : ℕ} [decidable_pred Q] (hPQ : P ≤ Q) (hab : a ≤ b) :
+  nat.find_greatest P a ≤ nat.find_greatest Q b :=
+(nat.find_greatest_mono_right _ hab).trans $ find_greatest_mono_left hPQ _
+
+lemma find_greatest_is_greatest (hk : nat.find_greatest P b < k) (hkb : k ≤ b) : ¬ P k :=
 (find_greatest_eq_iff.1 rfl).2.2 hk hkb
 
-lemma find_greatest_of_ne_zero {b m} (h : nat.find_greatest P b = m) (h0 : m ≠ 0) : P m :=
+lemma find_greatest_of_ne_zero (h : nat.find_greatest P b = m) (h0 : m ≠ 0) : P m :=
 (find_greatest_eq_iff.1 h).2.1 h0
 
 end find_greatest

src/measure_theory/measurable_space.lean

@@ -299,9 +299,9 @@ lemma measurable_to_nat {f : α → ℕ} : (∀ y, measurable_set (f ⁻¹' {f y
 measurable_to_encodable
 
 lemma measurable_find_greatest' {p : α → ℕ → Prop}
-  {N} (hN : ∀ k ≤ N, measurable_set {x | nat.find_greatest (p x) N = k}) :
+  {N : ℕ} (hN : ∀ k ≤ N, measurable_set {x | nat.find_greatest (p x) N = k}) :
   measurable (λ x, nat.find_greatest (p x) N) :=
-measurable_to_nat $ λ x, hN _ nat.find_greatest_le
+measurable_to_nat $ λ x, hN _ N.find_greatest_le
 
 lemma measurable_find_greatest {p : α → ℕ → Prop} {N} (hN : ∀ k ≤ N, measurable_set {x | p x k}) :
   measurable (λ x, nat.find_greatest (p x) N) :=