-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p = none) :
    ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
i : Nat
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
⊢ match (x :: xs)[i]? with
  | some a => p a = false
  | none => True

Tactic:
cases i with
| zero =>
  split at w <;> simp_all
| succ i =>
  simp only [getElem?_cons_succ]
  apply ih
  split at w <;> simp_all

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
i : Nat
⊢ match (x :: xs)[i + 1]? with
  | some a => p a = false
  | none => True

Tactic:
simp only [getElem?_cons_succ]

Result:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
i : Nat
⊢ match xs[i]? with
  | some a => p a = false
  | none => True

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => ¬p a = true
      | none => true = true
w : findIdx? p (x :: xs) = none
i : Nat
⊢ match (x :: xs)[i]? with
  | some a => ¬p a = true
  | none => true = true

Tactic:
simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
i : Nat
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
⊢ match (x :: xs)[i]? with
  | some a => p a = false
  | none => True

Proof state:
case nil
α : Type u_1
p : α → Bool
w : findIdx? p [] = none
i : Nat
⊢ match [][i]? with
  | some a => ¬p a = true
  | none => true = true

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
i : Nat
⊢ match xs[i]? with
  | some a => p a = false
  | none => True

Tactic:
apply ih

Result:
case cons.succ.w
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
i : Nat
⊢ findIdx? p xs = none

Proof state:
α : Type u_1
xs : List α
p : α → Bool
w : findIdx? p xs = none
⊢ ∀ (i : Nat),
    match xs[i]? with
    | some a => ¬p a = true
    | none => true = true

Tactic:
intro i

Result:
α : Type u_1
xs : List α
p : α → Bool
w : findIdx? p xs = none
i : Nat
⊢ match xs[i]? with
  | some a => ¬p a = true
  | none => true = true

Proof state:
case cons.succ.w
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
i : Nat
⊢ findIdx? p xs = none

Tactic:
split at w <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
w : findIdx? p xs = none
i : Nat
⊢ match xs[i]? with
  | some a => ¬p a = true
  | none => true = true

Tactic:
induction xs generalizing i with
| nil => simp_all
| cons x xs ih =>
  simp_all only [Bool.not_eq_true, findIdx?_cons, Nat.zero_add]
  cases i with
  | zero =>
    split at w <;> simp_all
  | succ i =>
    simp only [getElem?_cons_succ]
    apply ih
    split at w <;> simp_all

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs = none →
    ∀ (i : Nat),
      match xs[i]? with
      | some a => p a = false
      | none => True
w : (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = none
⊢ match (x :: xs)[0]? with
  | some a => p a = false
  | none => True

Tactic:
split at w <;> simp_all

Result:
no goals