m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
⊢ False
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
⊢ False
rw [find] at hi
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ False

case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
⊢ False
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with k
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hi : i ∈ if x : p (last n) then some (last n) else none
⊢ False
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ False
simp only [h] at hi
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ False

case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ False
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hi : i ∈ if x : p (last n) then some (last n) else none
⊢ False
split_ifs at hi with hl
case none.inl.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ False
cases hi
case none.inl.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : ∀ (i : Fin n), ¬p (castLT i (_ : ↑i < Nat.succ n))
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
case none.inl.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
rw [find_eq_none_iff] at h
no goals
case none.inl.refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
h : ∀ (i : Fin n), ¬p (castLT i (_ : ↑i < Nat.succ n))
hl : p (last n)
hj : { val := j, isLt := hjn } < last n
⊢ False
refine h ⟨j, hj⟩ hpj
no goals
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ False
exact Option.not_mem_none _ hi
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi :
  i ∈
    Option.casesOn (some k) (if x : p (last n) then some (last n) else none) fun i =>
      some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) (if x : p (last n) then some (last n) else none)
      fun i => some (castLT i (_ : ↑i < Nat.succ n))
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
rw [h] at hi
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi : i ∈ some (castLT k (_ : ↑k < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi :
  i ∈
    Option.casesOn (some k) (if x : p (last n) then some (last n) else none) fun i =>
      some (castLT i (_ : ↑i < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
dsimp at hi
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
hj : { val := j, isLt := hjn } < castLT k (_ : ↑k < Nat.succ n)
hi : castLT k (_ : ↑k < Nat.succ n) ∈ some (castLT k (_ : ↑k < Nat.succ n))
⊢ False
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : { val := j, isLt := hjn } < i
hpj : p { val := j, isLt := hjn }
k : Fin n
hi : i ∈ some (castLT k (_ : ↑k < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
⊢ False
obtain rfl := Option.some_inj.1 hi
no goals
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p { val := j, isLt := hjn }
k : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some k
hj : { val := j, isLt := hjn } < castLT k (_ : ↑k < Nat.succ n)
hi : castLT k (_ : ↑k < Nat.succ n) ∈ some (castLT k (_ : ↑k < Nat.succ n))
⊢ False
exact find_min h (show (⟨j, lt_trans hj k.2⟩ : Fin n) < k from hj) hpj