-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_findSome?_zipIdx {xs : List α} {p : α → Bool} :
    xs.findIdx? p = xs.zipIdx.findSome? fun ⟨a, i⟩ => if p a then some i else none

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
h✝ : p x = true
⊢ some 0 = findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)

case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)

Tactic:
simp_all only [zipIdx_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) (xs.zipIdx 1)

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) (map (Prod.map id fun x => x + 1) xs.zipIdx)

Tactic:
simp [Function.comp_def, findSome?_map]

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) (xs.zipIdx 1)

Tactic:
rw [← map_snd_add_zipIdx_eq_zipIdx (n := 1) (k := 0)]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : findIdx? p xs = findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findSome? (fun x => if p x.fst = true then some x.snd else none) xs.zipIdx) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) (map (Prod.map id fun x => x + 1) xs.zipIdx)

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
h✝ : p x = true
⊢ some 0 = findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx? p [] =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      [].zipIdx

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
⊢ findIdx? p (x :: xs) =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      (x :: xs).zipIdx

Tactic:
simp only [findIdx?_cons, Nat.zero_add, zipIdx]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    findSome?
      (fun x =>
        match x with
        | (a, i) => if p a = true then some i else none)
      xs.zipIdx
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) =
    findSome? (fun x => if p x.fst = true then some x.snd else none) ((x, 0) :: xs.zipIdx 1)