-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
    List.findIdx?.go p xs i =
      (List.findFinIdx?.go p l xs i h).map (·.val)

Proof state:
case h_2
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
⊢ (if p a = true then some i else findIdx?.go p xs (i + 1)) =
    Option.map (fun x => ↑x)
      (match a :: xs, i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

Tactic:
simp only

Result:
case h_2
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
⊢ (if p a = true then some i else findIdx?.go p xs (i + 1)) =
    Option.map (fun x => ↑x) (if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l xs (i + 1) ⋯)

Proof state:
case h_2
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
⊢ (if p a = true then some i else findIdx?.go p xs (i + 1)) =
    Option.map (fun x => ↑x) (if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l xs (i + 1) ⋯)

Tactic:
split

Result:
case h_2.isTrue
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
h✝ : p a = true
⊢ some i = Option.map (fun x => ↑x) (some ⟨i, ⋯⟩)

case h_2.isFalse
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
h✝ : ¬p a = true
⊢ findIdx?.go p xs (i + 1) = Option.map (fun x => ↑x) (findFinIdx?.go p l xs (i + 1) ⋯)

Proof state:
α : Type u_1
l xs : List α
p : α → Bool
i : Nat
h : xs.length + i = l.length
⊢ findIdx?.go p xs i = Option.map (fun x => ↑x) (findFinIdx?.go p l xs i h)

Tactic:
unfold findIdx?.go

Result:
α : Type u_1
l xs : List α
p : α → Bool
i : Nat
h : xs.length + i = l.length
⊢ (match xs, i with
    | [], x => none
    | a :: l, i => if p a = true then some i else findIdx?.go p l (i + 1)) =
    Option.map (fun x => ↑x) (findFinIdx?.go p l xs i h)

Proof state:
α : Type u_1
l xs : List α
p : α → Bool
i : Nat
h : xs.length + i = l.length
⊢ (match xs, i with
    | [], x => none
    | a :: l, i => if p a = true then some i else findIdx?.go p l (i + 1)) =
    Option.map (fun x => ↑x) (findFinIdx?.go p l xs i h)

Tactic:
unfold findFinIdx?.go

Result:
α : Type u_1
l xs : List α
p : α → Bool
i : Nat
h : xs.length + i = l.length
⊢ (match xs, i with
    | [], x => none
    | a :: l, i => if p a = true then some i else findIdx?.go p l (i + 1)) =
    Option.map (fun x => ↑x)
      (match xs, i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

Proof state:
case h_2.isTrue
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
h✝ : p a = true
⊢ some i = Option.map (fun x => ↑x) (some ⟨i, ⋯⟩)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l xs : List α
p : α → Bool
i : Nat
h : xs.length + i = l.length
⊢ (match xs, i with
    | [], x => none
    | a :: l, i => if p a = true then some i else findIdx?.go p l (i + 1)) =
    Option.map (fun x => ↑x)
      (match xs, i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

Tactic:
split <;> rename_i a xs

Result:
case h_1
α : Type u_1
l : List α
p : α → Bool
i : Nat
a : List α
xs : Nat
h : [].length + i = l.length
⊢ none =
    Option.map (fun x => ↑x)
      (match [], i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

case h_2
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
⊢ (if p a = true then some i else findIdx?.go p xs (i + 1)) =
    Option.map (fun x => ↑x)
      (match a :: xs, i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

Proof state:
case h_2.isFalse
α : Type u_1
l : List α
p : α → Bool
i : Nat
x✝¹ : List α
x✝ : Nat
a : α
xs : List α
h : (a :: xs).length + i = l.length
h✝ : ¬p a = true
⊢ findIdx?.go p xs (i + 1) = Option.map (fun x => ↑x) (findFinIdx?.go p l xs (i + 1) ⋯)

Tactic:
rw [findIdx?_go_eq_map_findFinIdx?_go_val]

Result:
no goals

Proof state:
case h_1
α : Type u_1
l : List α
p : α → Bool
i : Nat
a : List α
xs : Nat
h : [].length + i = l.length
⊢ none =
    Option.map (fun x => ↑x)
      (match [], i, h with
      | [], x, x_1 => none
      | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else findFinIdx?.go p l l_1 (i + 1) ⋯)

Tactic:
simp_all

Result:
no goals