-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Lemmas.lean
theorem eq_none_of_findSome?_eq_none {f : Fin n → Option α} (h : findSome? f = none) (i) :
    f i = none

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

Tactic:
match heq : f 0 with
| some x =>
  rw [heq, Option.some_orElse] at h
  contradiction
| none =>
  rw [heq, Option.none_orElse] at h
  cases i using Fin.cases with
  | zero => exact heq
  | succ i => exact ih h i

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → Option α
h : findSome? f = none
i : Fin n
⊢ f i = none

Tactic:
induction n with
| zero => cases i; contradiction
| succ n ih =>
  rw [findSome?_succ] at h
  match heq : f 0 with
  | some x =>
    rw [heq, Option.some_orElse] at h
    contradiction
  | none =>
    rw [heq, Option.none_orElse] at h
    cases i using Fin.cases with
    | zero => exact heq
    | succ i => exact ih h i

Result:
no goals

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

Tactic:
exact ih h i

Result:
no goals

Proof state:
case zero
α : Type u_1
f : Fin 0 → Option α
h : findSome? f = none
i : Fin 0
⊢ f i = none

Tactic:
cases i

Result:
case zero.mk
α : Type u_1
f : Fin 0 → Option α
h : findSome? f = none
val✝ : Nat
isLt✝ : val✝ < 0
⊢ f ⟨val✝, isLt✝⟩ = none

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

Tactic:
exact heq

Result:
no goals

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

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

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

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

Tactic:
rw [findSome?_succ] at h

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

Proof state:
case zero.mk
α : Type u_1
f : Fin 0 → Option α
h : findSome? f = none
val✝ : Nat
isLt✝ : val✝ < 0
⊢ f ⟨val✝, isLt✝⟩ = none

Tactic:
contradiction

Result:
no goals

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

Tactic:
cases i using Fin.cases with
| zero => exact heq
| succ i => exact ih h i

Result:
no goals

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

Tactic:
contradiction

Result:
no goals

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

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

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