-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
    findIdx?.go p xs (i+1) = (findIdx?.go p xs 0).map fun k => k + (i + 1)

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
h✝ : p head✝ = true
⊢ Option.map (fun i => i + 1) (some i) = Option.map (fun k => k + (i + 1)) (some 0)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.e_f
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
⊢ ((fun i => i + 1) ∘ fun k => k + (i + 1)) = (fun k => k + (i + 1)) ∘ fun k => k + 1

Tactic:
ext

Result:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
x✝ : Nat
⊢ ((fun i => i + 1) ∘ fun k => k + (i + 1)) x✝ = ((fun k => k + (i + 1)) ∘ fun k => k + 1) x✝

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
h✝ : ¬p head✝ = true
⊢ Option.map (fun i => i + 1) (Option.map (fun i => i + 1) (findIdx?.go p tail✝ i)) =
    Option.map (fun k => k + (i + 1)) (Option.map (fun i => i + 1) (findIdx?.go p tail✝ 0))

Tactic:
simp_all only [findIdx?_go_succ, Bool.not_eq_true, Option.map_map, Nat.zero_add]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
⊢ Option.map ((fun i => i + 1) ∘ fun k => k + (i + 1)) (findIdx?.go p tail✝ 0) =
    Option.map ((fun k => k + (i + 1)) ∘ fun k => k + 1) (findIdx?.go p tail✝ 0)

Proof state:
case cons.isFalse.e_f.h
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
x✝ : Nat
⊢ ((fun i => i + 1) ∘ fun k => k + (i + 1)) x✝ = ((fun k => k + (i + 1)) ∘ fun k => k + 1) x✝

Tactic:
simp only [Nat.add_comm i, Function.comp_apply, Nat.add_assoc]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
⊢ findIdx?.go p (head✝ :: tail✝) (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p (head✝ :: tail✝) 0)

Tactic:
simp only [findIdx?_go_succ, findIdx?_go_cons, Nat.zero_add]

Result:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
⊢ Option.map (fun i => i + 1) (if p head✝ = true then some i else Option.map (fun i => i + 1) (findIdx?.go p tail✝ i)) =
    Option.map (fun k => k + (i + 1))
      (if p head✝ = true then some 0 else Option.map (fun i => i + 1) (findIdx?.go p tail✝ 0))

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
⊢ findIdx?.go p [] (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p [] 0)

Tactic:
simp

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
⊢ Option.map ((fun i => i + 1) ∘ fun k => k + (i + 1)) (findIdx?.go p tail✝ 0) =
    Option.map ((fun k => k + (i + 1)) ∘ fun k => k + 1) (findIdx?.go p tail✝ 0)

Tactic:
congr

Result:
case cons.isFalse.e_f
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
i : Nat
tail_ih✝ :
  ∀ {i : Nat},
    Option.map (fun i => i + 1) (findIdx?.go p tail✝ i) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
h✝ : p head✝ = false
⊢ ((fun i => i + 1) ∘ fun k => k + (i + 1)) = (fun k => k + (i + 1)) ∘ fun k => k + 1

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
⊢ Option.map (fun i => i + 1) (if p head✝ = true then some i else Option.map (fun i => i + 1) (findIdx?.go p tail✝ i)) =
    Option.map (fun k => k + (i + 1))
      (if p head✝ = true then some 0 else Option.map (fun i => i + 1) (findIdx?.go p tail✝ 0))

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
h✝ : p head✝ = true
⊢ Option.map (fun i => i + 1) (some i) = Option.map (fun k => k + (i + 1)) (some 0)

case cons.isFalse
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {i : Nat}, findIdx?.go p tail✝ (i + 1) = Option.map (fun k => k + (i + 1)) (findIdx?.go p tail✝ 0)
i : Nat
h✝ : ¬p head✝ = true
⊢ Option.map (fun i => i + 1) (Option.map (fun i => i + 1) (findIdx?.go p tail✝ i)) =
    Option.map (fun k => k + (i + 1)) (Option.map (fun i => i + 1) (findIdx?.go p tail✝ 0))