no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
l : List α
⊢ filterMap g (filterMap f l) = filterMap (fun x => Option.bind (f x) g) l
induction l with
| nil => rfl
| cons a l IH => cases h : f a <;> simp [*]
no goals
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
⊢ filterMap g (filterMap f []) = filterMap (fun x => Option.bind (f x) g) []
rfl
no goals
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → Option γ
a : α
l : List α
IH : filterMap g (filterMap f l) = filterMap (fun x => Option.bind (f x) g) l
⊢ filterMap g (filterMap f (a :: l)) = filterMap (fun x => Option.bind (f x) g) (a :: l)
cases h : f a <;> simp [*]