-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem findIdx?_take {xs : List α} {n : Nat} {p : α → Bool} :
    (xs.take n).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun i => i < n))

Proof state:
case nil
α : Type u_1
p : α → Bool
n : Nat
⊢ findIdx? p (take n []) = (findIdx? p []).bind (Option.guard fun i => i < n)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n : Nat
⊢ findIdx? p (take n (x :: xs)) = (findIdx? p (x :: xs)).bind (Option.guard fun i => i < n)

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
⊢ findIdx? p (take 0 (x :: xs)) = (findIdx? p (x :: xs)).bind (Option.guard fun i => i < 0)

case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
⊢ findIdx? p (take (n✝ + 1) (x :: xs)) = (findIdx? p (x :: xs)).bind (Option.guard fun i => i < n✝ + 1)

Proof state:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
h✝ : p x = true
⊢ some 0 = (some 0).bind (Option.guard fun i => i < n✝ + 1)

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p (take n✝ xs)) =
    (Option.map (fun i => i + 1) (findIdx? p xs)).bind (Option.guard fun i => i < n✝ + 1)

Tactic:
simp [ih, Option.guard_comp, Option.bind_map]

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
⊢ findIdx? p (take 0 (x :: xs)) = (findIdx? p (x :: xs)).bind (Option.guard fun i => i < 0)

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (take n✝ xs))) =
    (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).bind (Option.guard fun i => i < n✝ + 1)

Tactic:
split

Result:
case cons.succ.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
h✝ : p x = true
⊢ some 0 = (some 0).bind (Option.guard fun i => i < n✝ + 1)

case cons.succ.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p (take n✝ xs)) =
    (Option.map (fun i => i + 1) (findIdx? p xs)).bind (Option.guard fun i => i < n✝ + 1)

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
⊢ findIdx? p (take (n✝ + 1) (x :: xs)) = (findIdx? p (x :: xs)).bind (Option.guard fun i => i < n✝ + 1)

Tactic:
simp only [take_succ_cons, findIdx?_cons]

Result:
case cons.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {n : Nat}, findIdx? p (take n xs) = (findIdx? p xs).bind (Option.guard fun i => i < n)
n✝ : Nat
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p (take n✝ xs))) =
    (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)).bind (Option.guard fun i => i < n✝ + 1)