m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P (n + 1)
m n k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ Monotone (Nat.findGreatest P)
refine monotone_nat_of_le_succ fun n => ?_
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ if P (n + 1) then n + 1 else Nat.findGreatest P n
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P (n + 1)
rw [findGreatest_succ]
case inl
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : P (n + 1)
⊢ Nat.findGreatest P n ≤ n + 1

case inr
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : ¬P (n + 1)
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P n
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ if P (n + 1) then n + 1 else Nat.findGreatest P n
split_ifs
no goals
case inl
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : P (n + 1)
⊢ Nat.findGreatest P n ≤ n + 1
exact (findGreatest_le n).trans (le_succ _)
no goals
case inr
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : ¬P (n + 1)
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P n
rfl