case h
α : Type u_1
p : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l
α : Type u_1
p : α → Bool
⊢ filterMap (Option.guard fun x => p x = true) = filter p
funext l
no goals
case h
α : Type u_1
p : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => p x = true) l = filter p l
induction l with
| nil => rfl
| cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, ← IH]
no goals
case h.nil
α : Type u_1
p : α → Bool
⊢ filterMap (Option.guard fun x => p x = true) [] = filter p []
rfl
no goals
case h.cons
α : Type u_1
p : α → Bool
a : α
l : List α
IH : filterMap (Option.guard fun x => p x = true) l = filter p l
⊢ filterMap (Option.guard fun x => p x = true) (a :: l) = filter p (a :: l)
by_cases pa : p a <;> simp [Option.guard, pa, ← IH]