-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem exists_of_findSome?_eq_some {f : Fin n → Option α} (h : findSome? f = some x) :
    ∃ i, f i = some x

Proof state:
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (findSome? fun i => f i.succ) = some x
heq : f 0 = none
⊢ ∃ i, f i = some x

Tactic:
match ih h with | ⟨i, _⟩ => exists i.succ

Result:
no goals

Proof state:
case zero
α : Type u_1
x : α
f : Fin 0 → Option α
h : none = some x
⊢ ∃ i, f i = some x

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (f 0 <|> findSome? fun i => f i.succ) = some x
⊢ ∃ i, f i = some x

Tactic:
match heq : f 0 with
| some x =>
  rw [heq, Option.some_orElse] at h
  exists 0
  rw [heq, h]
| none =>
  rw [heq, Option.none_orElse] at h
  match ih h with | ⟨i, _⟩ => exists i.succ

Result:
no goals

Proof state:
case zero
α : Type u_1
x : α
f : Fin 0 → Option α
h : findSome? f = some x
⊢ ∃ i, f i = some x

Tactic:
rw [findSome?_zero] at h

Result:
case zero
α : Type u_1
x : α
f : Fin 0 → Option α
h : none = some x
⊢ ∃ i, f i = some x

Proof state:
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (f 0 <|> findSome? fun i => f i.succ) = some x
heq : f 0 = none
⊢ ∃ i, f i = some x

Tactic:
rw [heq, Option.none_orElse] at h

Result:
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (findSome? fun i => f i.succ) = some x
heq : f 0 = none
⊢ ∃ i, f i = some x

Proof state:
α : Type u_1
x✝ : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x✝ → ∃ i, f i = some x✝
f : Fin (n + 1) → Option α
x : α
h : some x = some x✝
heq : f 0 = some x
⊢ f 0 = some x✝

Tactic:
rw [heq, h]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
x : α
f : Fin n → Option α
h : findSome? f = some x
⊢ ∃ i, f i = some x

Tactic:
induction n with
| zero => rw [findSome?_zero] at h; contradiction
| succ n ih =>
  rw [findSome?_succ] at h
  match heq : f 0 with
  | some x =>
    rw [heq, Option.some_orElse] at h
    exists 0
    rw [heq, h]
  | none =>
    rw [heq, Option.none_orElse] at h
    match ih h with | ⟨i, _⟩ => exists i.succ

Result:
no goals

Proof state:
α : Type u_1
x✝ : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x✝ → ∃ i, f i = some x✝
f : Fin (n + 1) → Option α
h : (f 0 <|> findSome? fun i => f i.succ) = some x✝
x : α
heq : f 0 = some x
⊢ ∃ i, f i = some x✝

Tactic:
rw [heq, Option.some_orElse] at h

Result:
α : Type u_1
x✝ : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x✝ → ∃ i, f i = some x✝
f : Fin (n + 1) → Option α
x : α
h : some x = some x✝
heq : f 0 = some x
⊢ ∃ i, f i = some x✝

Proof state:
α : Type u_1
x✝ : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x✝ → ∃ i, f i = some x✝
f : Fin (n + 1) → Option α
x : α
h : some x = some x✝
heq : f 0 = some x
⊢ ∃ i, f i = some x✝

Tactic:
exists 0

Result:
α : Type u_1
x✝ : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x✝ → ∃ i, f i = some x✝
f : Fin (n + 1) → Option α
x : α
h : some x = some x✝
heq : f 0 = some x
⊢ f 0 = some x✝

Proof state:
case succ
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : findSome? f = some x
⊢ ∃ i, f i = some x

Tactic:
rw [findSome?_succ] at h

Result:
case succ
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (f 0 <|> findSome? fun i => f i.succ) = some x
⊢ ∃ i, f i = some x

Proof state:
α : Type u_1
x : α
n : Nat
ih : ∀ {f : Fin n → Option α}, findSome? f = some x → ∃ i, f i = some x
f : Fin (n + 1) → Option α
h : (findSome? fun i => f i.succ) = some x
heq : f 0 = none
i : Fin n
h✝ : f i.succ = some x
⊢ ∃ i, f i = some x

Tactic:
exists i.succ

Result:
no goals