case intro
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
⊢ i ∈ find p
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
⊢ (p i ∧ ∀ (j : Fin n), p j → i ≤ j) → i ∈ find p
rintro ⟨hpi, hj⟩
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : find p = none
⊢ i ∈ none

case intro.some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
val✝ : Fin n
hfp : find p = some val✝
⊢ i ∈ some val✝
case intro
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
⊢ i ∈ find p
cases hfp : Fin.find p
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : ∀ (i : Fin n), ¬p i
⊢ i ∈ none
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : find p = none
⊢ i ∈ none
rw [find_eq_none_iff] at hfp
no goals
case intro.none
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
hfp : ∀ (i : Fin n), ¬p i
⊢ i ∈ none
exact (hfp _ hpi).elim
no goals
case intro.some
m n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
i : Fin n
hpi : p i
hj : ∀ (j : Fin n), p j → i ≤ j
val✝ : Fin n
hfp : find p = some val✝
⊢ i ∈ some val✝
exact Option.some_inj.2 (le_antisymm (find_min' hfp hpi) (hj _ (find_spec _ hfp)))