no goals
α : Type u
β : Type v
γ : Type w
a : α
r : List (List α)
⊢ sublistsAux a [] = List.bind [] fun l => [l, a :: l]
simp [sublistsAux]
α : Type u
β : Type v
γ : Type w
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = List.bind r fun l => [l, a :: l]
⊢ foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
α : Type u
β : Type v
γ : Type w
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = List.bind r fun l => [l, a :: l]
⊢ sublistsAux a (r ++ [l]) = List.bind (r ++ [l]) fun l => [l, a :: l]
rw [bind_append, ← ih, bind_singleton, sublistsAux, foldl_append]
no goals
α : Type u
β : Type v
γ : Type w
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = List.bind r fun l => [l, a :: l]
⊢ foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
simp [sublistsAux]