-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
    (l.filterMap f).takeWhile p = (l.takeWhile fun a => (f a).all p).filterMap f

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ takeWhile p (b✝ :: filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Tactic:
simp [takeWhile_cons, h, ih]

Result:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ (if p b✝ = true then b✝ :: filterMap f (takeWhile (fun a => Option.all p (f a)) xs) else []) =
    filterMap f (if p b✝ = true then x :: takeWhile (fun a => Option.all p (f a)) xs else [])

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
h : f x = none
⊢ takeWhile p (filterMap f xs) =
    filterMap f (if Option.all p none = true then x :: takeWhile (fun a => Option.all p (f a)) xs else [])

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
⊢ takeWhile p
      (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs) =
    filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Tactic:
split <;> rename_i h

Result:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
h : f x = none
⊢ takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ takeWhile p (b✝ :: filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Proof state:
case cons.h_2
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ (if p b✝ = true then b✝ :: filterMap f (takeWhile (fun a => Option.all p (f a)) xs) else []) =
    filterMap f (if p b✝ = true then x :: takeWhile (fun a => Option.all p (f a)) xs else [])

Tactic:
split <;> simp_all [filterMap_cons]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
⊢ takeWhile p (filterMap f (x :: xs)) = filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Tactic:
simp only [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
⊢ takeWhile p
      (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs) =
    filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
⊢ takeWhile p (filterMap f []) = filterMap f (takeWhile (fun a => Option.all p (f a)) [])

Tactic:
rfl

Result:
no goals

Proof state:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
h : f x = none
⊢ takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) (x :: xs))

Tactic:
simp only [takeWhile_cons, h]

Result:
case cons.h_1
α : Type u_1
β : Type u_2
f : α → Option β
p : β → Bool
x : α
xs : List α
ih : takeWhile p (filterMap f xs) = filterMap f (takeWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
h : f x = none
⊢ takeWhile p (filterMap f xs) =
    filterMap f (if Option.all p none = true then x :: takeWhile (fun a => Option.all p (f a)) xs else [])