-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem find_spec :
    ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p), p i
  | 0, _, _, _, hi => Option.noConfusion hi
  | n + 1, p, I, i, hi => by
    rw [find] at hi
    rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
    · rw [h] at hi
      dsimp at hi
      split_ifs at hi with hl
      · simp only [Option.mem_def, Option.some.injEq] at hi
        exact hi ▸ hl
      · exact (Option.not_mem_none _ hi).elim
    · rw [h] at hi
      dsimp at hi
      rw [← Option.some_inj.1 hi]
      exact @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (j.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p (j.castLT ⋯)

Tactic:
exact @find_spec n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _ _ h

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
⊢ p i

Tactic:
rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j

Result:
case none
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = none
⊢ p i

case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : Fin n
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Proof state:
case none
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 (i.castLT ⋯)) = none
⊢ p i

Tactic:
split_ifs at hi with hl

Result:
case pos
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ p i

case neg
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ p i

Proof state:
case neg
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ p i

Tactic:
exact (Option.not_mem_none _ hi).elim

Result:
no goals

Proof state:
case pos
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ p i

Tactic:
simp only [Option.mem_def, Option.some.injEq] at hi

Result:
case pos
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : last n = i
⊢ p i

Proof state:
case none
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 (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = none
⊢ p i

Tactic:
dsimp at hi

Result:
case none
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 (i.castLT ⋯)) = none
⊢ p i

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
⊢ p i

Tactic:
rw [find] at hi

Result:
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
⊢ p i

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : Fin n
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Tactic:
rw [h] at hi

Result:
case some
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 (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Proof state:
case pos
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : last n = i
⊢ p i

Tactic:
exact hi ▸ hl

Result:
no goals

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (j.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Tactic:
rw [← Option.some_inj.1 hi]

Result:
case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (j.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p (j.castLT ⋯)

Proof state:
case some
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 (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Tactic:
dsimp at hi

Result:
case some
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
j : Fin n
hi : i ∈ some (j.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ p i

Proof state:
case none
n : ℕ
p : Fin (n + 1) → Prop
I : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = none
⊢ p i

Tactic:
rw [h] at hi

Result:
case none
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 (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = none
⊢ p i