-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_fst_find?_zipIdx {xs : List α} {p : α → Bool} :
    xs.findIdx? p = (xs.zipIdx.find? fun ⟨x, _⟩ => p x).map (·.2)

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ findIdx? p [] =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        [].zipIdx)

Tactic:
simp

Result:
no goals

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

Tactic:
simp [Function.comp_def, *]

Result:
no goals

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

Tactic:
rw [ih, ← 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 =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1)
      (Option.map (fun x => x.snd)
        (find?
          (fun x =>
            match x with
            | (x, snd) => p x)
          xs.zipIdx)) =
    Option.map (fun x => x.snd) (find? (fun x => p x.fst) ((x, 0) :: 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 =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
h✝ : p x = true
⊢ some 0 = Option.map (fun x => x.snd) (find? (fun x => p x.fst) ((x, 0) :: xs.zipIdx 1))

Tactic:
simp_all

Result:
no goals

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

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
h✝ : p x = true
⊢ some 0 = Option.map (fun x => x.snd) (find? (fun x => p x.fst) ((x, 0) :: xs.zipIdx 1))

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

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih :
  findIdx? p xs =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        xs.zipIdx)
⊢ findIdx? p (x :: xs) =
    Option.map (fun x => x.snd)
      (find?
        (fun x =>
          match x with
          | (x, snd) => p x)
        (x :: xs).zipIdx)

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

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