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