m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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))
⊢ p i
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
⊢ p i
rw [find] at hi
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i

case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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 : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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))
⊢ p i
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with j
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn none (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))) = none
⊢ p i
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
rw [h] at hi
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ if p (last n) then some (last n) else none
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn none (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))) = none
⊢ p i
dsimp at hi
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ p i

case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ p i
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ if p (last n) then some (last n) else none
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ p i
split_ifs at hi with hl
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : last n = i
⊢ p i
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ p i
simp only [Option.mem_def, Option.some.injEq] at hi
no goals
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last n)
hi : last n = i
⊢ p i
exact hi ▸ hl
no goals
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ p i
exact (Option.not_mem_none _ hi).elim
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi :
  i ∈
    Option.casesOn (some j) (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 j
⊢ p i
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : 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 : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
rw [h] at hi
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi :
  i ∈
    Option.casesOn (some j) (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 j
⊢ p i
dsimp at hi
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p (castLT j (_ : ↑j < Nat.succ n))
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p i
rw [← Option.some_inj.1 hi]
no goals
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (castLT j (_ : ↑j < Nat.succ n))
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ p (castLT j (_ : ↑j < Nat.succ n))
refine @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h