P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P → ∀ (m : ℕ), m ≤ n → ¬P m
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P ↔ ∀ (m : ℕ), m ≤ n → ¬P m
refine' ⟨_, lt_find P n⟩
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
⊢ ¬P m
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ ↑n < find P → ∀ (m : ℕ), m ≤ n → ¬P m
intro h m hm
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ ¬P m

case neg
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : ¬(find P).Dom
⊢ ¬P m
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
⊢ ¬P m
by_cases H : (find P).Dom
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ ¬P m
apply Nat.find_min H
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (h : (find P).Dom), n < Part.get (find P) h
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
rw [coe_lt_iff] at h
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n m : ℕ
hm : m ≤ n
H : (find P).Dom
h : n < Part.get (find P) H
⊢ m < Nat.find H
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ∀ (h : (find P).Dom), n < Part.get (find P) h
m : ℕ
hm : m ≤ n
H : (find P).Dom
⊢ m < Nat.find H
specialize h H
no goals
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
n m : ℕ
hm : m ≤ n
H : (find P).Dom
h : n < Part.get (find P) H
⊢ m < Nat.find H
exact lt_of_le_of_lt hm h
no goals
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ↑n < find P
m : ℕ
hm : m ≤ n
H : ¬(find P).Dom
⊢ ¬P m
exact not_exists.mp H m