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