-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem isSome_find_iff :
    ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p], (find p).isSome ↔ ∃ i, p i
  | 0, _, _ => iff_of_false (fun h ↦ Bool.noConfusion h) fun ⟨i, _⟩ ↦ Fin.elim0 i
  | n + 1, p, _ =>
    ⟨fun h ↦ by
      rw [Option.isSome_iff_exists] at h
      obtain ⟨i, hi⟩ := h
      exact ⟨i, find_spec _ hi⟩, fun ⟨⟨i, hin⟩, hi⟩ ↦ by
      dsimp [find]
      rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | j
      · split_ifs with hl
        · exact Option.isSome_some
        · have := (@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
              ⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩
          rw [h] at this
          exact this
      · simp⟩

Proof state:
case refl
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hin : n < n + 1
hi : p ⟨n, hin⟩
⊢ False

Tactic:
exact hl hi

Result:
no goals

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
j : Fin n
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) (some j)).isSome = true

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯))
        (find fun i => p (i.castLT ⋯))).isSome =
    true

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
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) none).isSome = true

case some
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
j : Fin n
h : (find fun i => p (i.castLT ⋯)) = some j
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) (some j)).isSome = true

Proof state:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
this : none.isSome = true
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Tactic:
exact this

Result:
no goals

Proof state:
case intro
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : find p = some i
⊢ ∃ i, p i

Tactic:
exact ⟨i, find_spec _ hi⟩

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
⊢ (find p).isSome = true

Tactic:
dsimp [find]

Result:
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯))
        (find fun i => p (i.castLT ⋯))).isSome =
    true

Proof state:
case none
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
⊢ (Option.rec (if p (last n) then some (last n) else none) (fun val => some (val.castLT ⋯)) none).isSome = true

Tactic:
split_ifs with hl

Result:
case pos
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
⊢ (Option.rec (some (last n)) (fun val => some (val.castLT ⋯)) none).isSome = true

case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h✝ : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
h : i = n
⊢ False

Tactic:
cases h

Result:
case refl
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hin : n < n + 1
hi : p ⟨n, hin⟩
⊢ False

Proof state:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
this : (find fun x => p (x.castLT ⋯)).isSome = true
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Tactic:
rw [h] at this

Result:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
this : none.isSome = true
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Proof state:
case pos
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
⊢ (Option.rec (some (last n)) (fun val => some (val.castLT ⋯)) none).isSome = true

Tactic:
exact Option.isSome_some

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : (find p).isSome = true
⊢ ∃ i, p i

Tactic:
rw [Option.isSome_iff_exists] at h

Result:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : ∃ a, find p = some a
⊢ ∃ i, p i

Proof state:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Tactic:
have := (@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
    ⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩

Result:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p ⟨i, hin⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
this : (find fun x => p (x.castLT ⋯)).isSome = true
⊢ (Option.rec none (fun val => some (val.castLT ⋯)) none).isSome = true

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : ∃ a, find p = some a
⊢ ∃ i, p i

Tactic:
obtain ⟨i, hi⟩ := h

Result:
case intro
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : find p = some i
⊢ ∃ i, p i