case cons
α : Type u_1
β : Type u_2
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : map some (filterMap f tail✝) = filter (fun b => Option.isSome b) (map f tail✝)
⊢ map some
      (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) =
    filter (fun b => Option.isSome b) (f head✝ :: map f tail✝)
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ map some (filterMap f l) = filter (fun b => Option.isSome b) (map f l)
induction l <;> simp
no goals
case cons
α : Type u_1
β : Type u_2
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : map some (filterMap f tail✝) = filter (fun b => Option.isSome b) (map f tail✝)
⊢ map some
      (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) =
    filter (fun b => Option.isSome b) (f head✝ :: map f tail✝)
split <;> simp [*]