-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem dropWhile_filterMap (f : α → Option β) (p : β → Bool) (l : List α) :
    (l.filterMap f).dropWhile p = (l.dropWhile 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 : dropWhile p (filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ dropWhile p (b✝ :: filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) (x :: xs))

Tactic:
simp [dropWhile_cons, h, ih]

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

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

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

Tactic:
rfl

Result:
no goals

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

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 : dropWhile p (filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) xs)
⊢ dropWhile p
      (match f x with
      | none => filterMap f xs
      | some b => b :: filterMap f xs) =
    filterMap f (dropWhile (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 : dropWhile p (filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
h : f x = none
⊢ dropWhile p (filterMap f xs) = filterMap f (dropWhile (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 : dropWhile p (filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) xs)
x✝ : Option β
b✝ : β
h : f x = some b✝
⊢ dropWhile p (b✝ :: filterMap f xs) = filterMap f (dropWhile (fun a => Option.all p (f a)) (x :: xs))

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

Tactic:
simp only [dropWhile_cons, h]

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

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

Tactic:
split <;> simp_all

Result:
no goals