α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap (fun x => Option.bind (Option.guard (fun x => p x = true) x) f) l =
    filterMap (fun x => if p x = true then f x else none) l
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap f (filter p l) = filterMap (fun x => if p x = true then f x else none) l
rw [← filterMap_eq_filter, filterMap_filterMap]
case e_f
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ (fun x => Option.bind (Option.guard (fun x => p x = true) x) f) = fun x => if p x = true then f x else none
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap (fun x => Option.bind (Option.guard (fun x => p x = true) x) f) l =
    filterMap (fun x => if p x = true then f x else none) l
congr
case e_f.h
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
x : α
⊢ Option.bind (Option.guard (fun x => p x = true) x) f = if p x = true then f x else none
case e_f
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ (fun x => Option.bind (Option.guard (fun x => p x = true) x) f) = fun x => if p x = true then f x else none
funext x
no goals
case e_f.h
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
x : α
⊢ Option.bind (Option.guard (fun x => p x = true) x) f = if p x = true then f x else none
by_cases h : p x <;> simp [Option.guard, h]