no goals
α : Type u
β : Type v
γ : Type w
f : α → β
⊢ sublists (map f []) = map (map f) (sublists [])
simp
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ (List.bind (List.bind (sublists l) fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind (sublists l) fun x => [x, a :: x]) fun x => [map f x]
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ sublists (map f (a :: l)) = map (map f) (sublists (a :: l))
rw [map_cons, sublists_cons, bind_eq_bind, sublists_map f l, sublists_cons,
  bind_eq_bind, map_eq_bind, map_eq_bind]
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ (List.bind (List.bind (sublists l) fun x => [map f x]) fun x => [x, f a :: x]) =
    List.bind (List.bind (sublists l) fun x => [x, a :: x]) fun x => [map f x]
induction sublists l <;> simp [*]