m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    find p
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
⊢ { val := Nat.find h, isLt := (_ : Nat.find h < n) } ∈ find p
let ⟨i, hin, hi⟩ := h
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : find p = none
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none

case some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    some f
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    find p
cases' hf : find p with f
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : ∀ (i : Fin n), ¬p i
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : find p = none
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none
rw [find_eq_none_iff] at hf
no goals
case none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
hf : ∀ (i : Fin n), ¬p i
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    none
exact (hf ⟨i, hin⟩ hi).elim
case some.refine'_1
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ f ≤
    { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) }

case some.refine'_2
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ≤
    f
case some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ∈
    some f
refine' Option.some_inj.2 (le_antisymm _ _)
no goals
case some.refine'_1
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ f ≤
    { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) }
exact find_min' hf (Nat.find_spec h).snd
no goals
case some.refine'_2
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ { val := Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }),
      isLt := (_ : Nat.find (_ : ∃ i hin, p { val := i, isLt := hin }) < n) } ≤
    f
exact Nat.find_min' _ ⟨f.2, by convert find_spec p hf⟩
no goals
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ i hin, p { val := i, isLt := hin }
i : ℕ
hin : i < n
hi : p { val := i, isLt := hin }
f : Fin n
hf : find p = some f
⊢ p { val := ↑f, isLt := (_ : ↑f < n) }
convert find_spec p hf