Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.list.sublists
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Data.List.Perm

/-! # sublists

`List.Sublists` gives a list of all (not necessarily contiguous) sublists of a list.

This file contains basic results on this function.
-/
/-
Porting note: various auxiliary definitions such as `sublists'_aux` were left out of the port
because they were only used to prove properties of `sublists`, and these proofs have changed.
-/
universe u v w

variable {α: Type uα : Type u: Type (u+1)Type u} {β: Type vβ : Type v: Type (v+1)Type v} {γ: Type wγ : Type w: Type (w+1)Type w}

open Nat

namespace List

/-! ### sublists -/

@[simp]
theorem sublists'_nil: ∀ {α : Type u}, sublists' [] = [[]]sublists'_nil : sublists': {α : Type ?u.15} → List α → List (List α)sublists' (@nil: {α : Type ?u.17} → List αnil α: Type uα) = [[]: List ?m.23[]] :=
rfl: ∀ {α : Sort ?u.55} {a : α}, a = arfl
#align list.sublists'_nil List.sublists'_nil: ∀ {α : Type u}, sublists' [] = [[]]List.sublists'_nil

@[simp]
theorem sublists'_singleton: ∀ {α : Type u} (a : α), sublists' [a] = [[], [a]]sublists'_singleton (a: αa : α: Type uα) : sublists': {α : Type ?u.714} → List α → List (List α)sublists' [a: αa] = [[]: List ?m.725[], [a: αa]] :=
rfl: ∀ {α : Sort ?u.738} {a : α}, a = arfl
#align list.sublists'_singleton List.sublists'_singleton: ∀ {α : Type u} (a : α), sublists' [a] = [[], [a]]List.sublists'_singleton

#noalign list.map_sublists'_aux
#noalign list.sublists'_aux_append
#noalign list.sublists'_aux_eq_sublists'

--Porting note: Not the same as `sublists'_aux` from Lean3
/-- Auxiliary helper definiiton for `sublists'` -/
def sublists'Aux: α → List (List α) → List (List α) → List (List α)sublists'Aux (a: αa : α: Type uα) (r₁: List (List α)r₁ r₂: List (List α)r₂ : List: Type ?u.13573 → Type ?u.13573List (List: Type ?u.13574 → Type ?u.13574List α: Type uα)) : List: Type ?u.13581 → Type ?u.13581List (List: Type ?u.13582 → Type ?u.13582List α: Type uα) :=
r₁: List (List α)r₁.foldl: {α : Type ?u.13588} → {β : Type ?u.13587} → (α → β → α) → α → List β → αfoldl (init := r₂: List (List α)r₂) fun r: ?m.13600r l: ?m.13603l => r: ?m.13600r ++ [a: αa :: l: ?m.13603l]
#align list.sublists'_aux List.sublists'Aux: {α : Type u} → α → List (List α) → List (List α) → List (List α)List.sublists'Aux

theorem sublists'Aux_eq_array_foldl: ∀ {α : Type u} (a : α) (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))sublists'Aux_eq_array_foldl (a: αa : α: Type uα) : ∀ (r₁: List (List α)r₁ r₂: List (List α)r₂ : List: Type ?u.13796 → Type ?u.13796List (List: Type ?u.13797 → Type ?u.13797List α: Type uα)),
sublists'Aux: {α : Type ?u.13801} → α → List (List α) → List (List α) → List (List α)sublists'Aux a: αa r₁: List (List α)r₁ r₂: List (List α)r₂ = ((r₁: List (List α)r₁.toArray: {α : Type ?u.13804} → List α → Array αtoArray).foldl: {α : Type ?u.13809} →
{β : Type ?u.13808} → (β → α → β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ (Array.size as) → βfoldl (init := r₂: List (List α)r₂.toArray: {α : Type ?u.13834} → List α → Array αtoArray)
(fun r: ?m.13825r l: ?m.13828l => r: ?m.13825r.push: {α : Type ?u.13843} → Array α → α → Array αpush (a: αa :: l: ?m.13828l))).toList: {α : Type ?u.13839} → Array α → List αtoList := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: α∀ (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))intro r₁: List (List α)r₁ r₂: List (List α)r₂α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)sublists'Aux a r₁ r₂ =   Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))
α: Type uβ: Type vγ: Type wa: α∀ (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))rw [α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)sublists'Aux a r₁ r₂ =   Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))sublists'Aux: {α : Type ?u.13888} → α → List (List α) → List (List α) → List (List α)sublists'Aux,α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)foldl (fun r l => r ++ [a :: l]) r₂ r₁ =   Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁))) α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)sublists'Aux a r₁ r₂ =   Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))Array.foldl_eq_foldl_data: ∀ {β : Type ?u.13889} {α : Type ?u.13890} (f : β → α → β) (init : β) (arr : Array α),
Array.foldl f init arr 0 (Array.size arr) = foldl f init arr.dataArray.foldl_eq_foldl_dataα: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)foldl (fun r l => r ++ [a :: l]) r₂ r₁ =   Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)]α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)foldl (fun r l => r ++ [a :: l]) r₂ r₁ =   Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)
α: Type uβ: Type vγ: Type wa: α∀ (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))have := List.foldl_hom: ∀ {α₁ : Type ?u.13945} {α₂ : Type ?u.13946} {β : Type ?u.13947} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂)
(l : List β) (init : α₁), (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → foldl g₂ (f init) l = f (foldl g₁ init l)List.foldl_hom Array.toList: {α : Type ?u.13951} → Array α → List αArray.toList (fun r: ?m.13957r l: ?m.13960l => r: ?m.13957r.push: {α : Type ?u.13962} → Array α → α → Array αpush (a: αa :: l: ?m.13960l))
(fun r: ?m.13978r l: ?m.13981l => r: ?m.13978r ++ [a: αa :: l: ?m.13981l]) r₁: List (List α)r₁ r₂: List (List α)r₂.toArray: {α : Type ?u.14032} → List α → Array αtoArray (α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)foldl (fun r l => r ++ [a :: l]) r₂ r₁ =   Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)∀ (x : Array (List α)) (y : List α),
(fun r l => r ++ [a :: l]) (Array.toList x) y = Array.toList ((fun r l => Array.push r (a :: l)) x y)simpGoals accomplished! 🐙)α: Type uβ: Type vγ: Type wa: αr₁, r₂: List (List α)this: foldl (fun r l => r ++ [a :: l]) (Array.toList (toArray r₂)) r₁ =   Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) r₁)foldl (fun r l => r ++ [a :: l]) r₂ r₁ =   Array.toList (foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁).data)
α: Type uβ: Type vγ: Type wa: α∀ (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))simpa using this: ?m.13944thisGoals accomplished! 🐙

theorem sublists'_eq_sublists'Aux: ∀ (l : List α), sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] lsublists'_eq_sublists'Aux (l: List αl : List: Type ?u.16547 → Type ?u.16547List α: Type uα) :
sublists': {α : Type ?u.16551} → List α → List (List α)sublists' l: List αl = l: List αl.foldr: {α : Type ?u.16556} → {β : Type ?u.16555} → (α → β → β) → β → List α → βfoldr (fun a: ?m.16565a r: ?m.16568r => sublists'Aux: {α : Type ?u.16570} → α → List (List α) → List (List α) → List (List α)sublists'Aux a: ?m.16565a r: ?m.16568r r: ?m.16568r) [[]: List ?m.16581[]] := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists' l = foldr (fun a r => sublists'Aux a r r) [[]] lsimp only [sublists': {α : Type ?u.16601} → List α → List (List α)sublists', sublists'Aux_eq_array_foldl: ∀ {α : Type ?u.16603} (a : α) (r₁ r₂ : List (List α)),
sublists'Aux a r₁ r₂ =     Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r₂) (toArray r₁) 0 (Array.size (toArray r₁)))sublists'Aux_eq_array_foldl]α: Type uβ: Type vγ: Type wl: List αArray.toList (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] l
α: Type uβ: Type vγ: Type wl: List αsublists' l = foldr (fun a r => sublists'Aux a r r) [[]] ldsimp onlyα: Type uβ: Type vγ: Type wl: List αArray.toList (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] l
α: Type uβ: Type vγ: Type wl: List αsublists' l = foldr (fun a r => sublists'Aux a r r) [[]] lrw [α: Type uβ: Type vγ: Type wl: List αArray.toList (foldr (fun a arr => Array.foldl (fun r l => Array.push r (a :: l)) arr arr 0 (Array.size arr)) #[[]] l) =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] l← List.foldr_hom: ∀ {β₁ : Type ?u.16819} {β₂ : Type ?u.16820} {α : Type ?u.16821} (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂)
(l : List α) (init : β₁), (∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) → foldr g₂ (f init) l = f (foldr g₁ init l)List.foldr_hom Array.toList: {α : Type ?u.16825} → Array α → List αArray.toListα: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) = Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))]α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) = Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))
α: Type uβ: Type vγ: Type wl: List αsublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l.α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] l α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList (Array.foldl (fun r l => Array.push r (a :: l)) (toArray r) (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) = Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l.α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y)) α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))intros _: ?m.16824_ _: Array ?m.16826_α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝));α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝)) α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push r (x :: l)) (toArray (Array.toList y)) (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList (Array.foldl (fun r l => Array.push r (x :: l)) y y 0 (Array.size y))congrα: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_4.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝))<;>α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_4.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push r (x✝ :: l)) (toArray (Array.toList y✝)) (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList (Array.foldl (fun r l => Array.push r (x✝ :: l)) y✝ y✝ 0 (Array.size y✝))simpGoals accomplished! 🐙

theorem sublists'Aux_eq_map: ∀ {α : Type u} (a : α) (r₁ r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁sublists'Aux_eq_map (a: αa : α: Type uα) (r₁: List (List α)r₁ : List: Type ?u.20930 → Type ?u.20930List (List: Type ?u.20931 → Type ?u.20931List α: Type uα)) : ∀ (r₂: List (List α)r₂ : List: Type ?u.20935 → Type ?u.20935List (List: Type ?u.20936 → Type ?u.20936List α: Type uα)),
sublists'Aux: {α : Type ?u.20940} → α → List (List α) → List (List α) → List (List α)sublists'Aux a: αa r₁: List (List α)r₁ r₂: List (List α)r₂ = r₂: List (List α)r₂ ++ map: {α : Type ?u.20947} → {β : Type ?u.20946} → (α → β) → List α → List βmap (cons: {α : Type ?u.20950} → α → List α → List αcons a: αa) r₁: List (List α)r₁ :=
List.reverseRecOn: ∀ {α : Type ?u.20998} {C : List α → Sort ?u.20997} (l : List α),
C [] → (∀ (l : List α) (a : α), C l → C (l ++ [a])) → C lList.reverseRecOn r₁: List (List α)r₁ (fun _: ?m.21029_ => byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αr₁, x✝: List (List α)sublists'Aux a [] x✝ = x✝ ++ map (cons a) []simp [sublists'Aux: {α : Type ?u.21053} → α → List (List α) → List (List α) → List (List α)sublists'Aux]Goals accomplished! 🐙) <| fun r₁: ?m.21035r₁ l: ?m.21038l ih: ?m.21041ih r₂: ?m.21045r₂ => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])rw [α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])map_append: ∀ {α : Type ?u.21161} {β : Type ?u.21162} (f : α → β) (l₁ l₂ : List α), map f (l₁ ++ l₂) = map f l₁ ++ map f l₂map_append,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ (map (cons a) r₁ ++ map (cons a) [l]) α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])map_singleton: ∀ {α : Type ?u.21181} {β : Type ?u.21182} (f : α → β) (a : α), map f [a] = [f a]map_singleton,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ (map (cons a) r₁ ++ [a :: l]) α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])← append_assoc: ∀ {α : Type ?u.21197} (as bs cs : List α), as ++ bs ++ cs = as ++ (bs ++ cs)append_assoc,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) r₁ ++ [a :: l] α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])← ih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁ih,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = sublists'Aux a r₁ r₂ ++ [a :: l] α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])sublists'Aux: {α : Type ?u.21231} → α → List (List α) → List (List α) → List (List α)sublists'Aux,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)foldl (fun r l => r ++ [a :: l]) r₂ (r₁ ++ [l]) = sublists'Aux a r₁ r₂ ++ [a :: l] α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])foldl_append: ∀ {α : Type ?u.21232} {β : Type ?u.21233} (f : β → α → β) (b : β) (l l' : List α),
foldl f b (l ++ l') = foldl f (foldl f b l) l'foldl_append,α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁) [l] = sublists'Aux a r₁ r₂ ++ [a :: l] α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])foldl: {α : Type ?u.21723} → {β : Type ?u.21722} → (α → β → α) → α → List β → αfoldlα: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =   sublists'Aux a r₁ r₂ ++ [a :: l]]α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =   sublists'Aux a r₁ r₂ ++ [a :: l]
α: Type uβ: Type vγ: Type wa: αr₁✝, r₁: List (List α)l: List αih: ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁r₂: List (List α)sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])simp [sublists'Aux: {α : Type ?u.21745} → α → List (List α) → List (List α) → List (List α)sublists'Aux]Goals accomplished! 🐙

-- Porting note: simp can prove `sublists'_singleton`
@[simp 900]
theorem sublists'_cons: ∀ (a : α) (l : List α), sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)sublists'_cons (a: αa : α: Type uα) (l: List αl : List: Type ?u.22065 → Type ?u.22065List α: Type uα) :
sublists': {α : Type ?u.22069} → List α → List (List α)sublists' (a: αa :: l: List αl) = sublists': {α : Type ?u.22078} → List α → List (List α)sublists' l: List αl ++ map: {α : Type ?u.22082} → {β : Type ?u.22081} → (α → β) → List α → List βmap (cons: {α : Type ?u.22085} → α → List α → List αcons a: αa) (sublists': {α : Type ?u.22092} → List α → List (List α)sublists' l: List αl) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αl: List αsublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)simp [sublists'_eq_sublists'Aux: ∀ {α : Type ?u.22136} (l : List α), sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] lsublists'_eq_sublists'Aux, foldr_cons: ∀ {α : Type ?u.22145} {β : Type ?u.22144} (f : α → β → β) (b : β) (a : α) (l : List α),
foldr f b (a :: l) = f a (foldr f b l)foldr_cons, sublists'Aux_eq_map: ∀ {α : Type ?u.22169} (a : α) (r₁ r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁sublists'Aux_eq_map]Goals accomplished! 🐙
#align list.sublists'_cons List.sublists'_cons: ∀ {α : Type u} (a : α) (l : List α), sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)List.sublists'_cons

@[simp]
theorem mem_sublists': ∀ {α : Type u} {s t : List α}, s ∈ sublists' t ↔ s <+ tmem_sublists' {s: List αs t: List αt : List: Type ?u.23106 → Type ?u.23106List α: Type uα} : s: List αs ∈ sublists': {α : Type ?u.23115} → List α → List (List α)sublists' t: List αt ↔ s: List αs <+ t: List αt := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ tinduction' t: List αt with a: ?m.23154a t: List ?m.23154t IH: ?m.23155 tIH generalizing s: List αsα: Type uβ: Type vγ: Type ws✝, s: List αnils ∈ sublists' [] ↔ s <+ []α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αconss ∈ sublists' (a :: t) ↔ s <+ a :: t
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ t·α: Type uβ: Type vγ: Type ws✝, s: List αnils ∈ sublists' [] ↔ s <+ [] α: Type uβ: Type vγ: Type ws✝, s: List αnils ∈ sublists' [] ↔ s <+ []α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αconss ∈ sublists' (a :: t) ↔ s <+ a :: tsimp only [sublists'_nil: ∀ {α : Type ?u.23185}, sublists' [] = [[]]sublists'_nil, mem_singleton: ∀ {α : Type ?u.23192} {a b : α}, a ∈ [b] ↔ a = bmem_singleton]α: Type uβ: Type vγ: Type ws✝, s: List αnils = [] ↔ s <+ []
α: Type uβ: Type vγ: Type ws✝, s: List αnils ∈ sublists' [] ↔ s <+ []exact ⟨fun h: ?m.23316h => α: Type uβ: Type vγ: Type ws✝, s: List αnils = [] ↔ s <+ []byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type ws✝, s: List αh: s = []s <+ []rw [α: Type uβ: Type vγ: Type ws✝, s: List αh: s = []s <+ []h: s = []hα: Type uβ: Type vγ: Type ws✝, s: List αh: s = [][] <+ []]Goals accomplished! 🐙, eq_nil_of_sublist_nil: ∀ {α : Type ?u.23322} {l : List α}, l <+ [] → l = []eq_nil_of_sublist_nil⟩Goals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ tsimp only [sublists'_cons: ∀ {α : Type ?u.23359} (a : α) (l : List α), sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)sublists'_cons, mem_append: ∀ {α : Type ?u.23367} {a : α} {s t : List α}, a ∈ s ++ t ↔ a ∈ s ∨ a ∈ tmem_append, IH: ?m.23155 tIH, mem_map: ∀ {α : Type ?u.23411} {β : Type ?u.23412} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = bmem_map]α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ tconstructorα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons.mp(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons.mprs <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t<;>α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons.mp(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons.mprs <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αcons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: tintro h: ?ahα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s;α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = scons.mps <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ trcases h: ?ah with (h | ⟨s, h, rfl⟩): ?a(h: s <+ thh | ⟨s, h, rfl⟩: ?a | ⟨s, h, rfl⟩: ∃ a_1, a_1 <+ t ∧ a :: a_1 = s⟨s: List αs⟨s, h, rfl⟩: ∃ a_1, a_1 <+ t ∧ a :: a_1 = s, h: s <+ th⟨s, h, rfl⟩: ∃ a_1, a_1 <+ t ∧ a :: a_1 = s, rfl: a :: s = s✝rfl⟨s, h, rfl⟩: ∃ a_1, a_1 <+ t ∧ a :: a_1 = s⟩(h | ⟨s, h, rfl⟩): ?a)α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inls <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inr.intro.introa :: s <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ t·α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inls <+ a :: t α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inls <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inr.intro.introa :: s <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = sexact sublist_cons_of_sublist: ∀ {α : Type ?u.23783} (a : α) {l₁ l₂ : List α}, l₁ <+ l₂ → l₁ <+ a :: l₂sublist_cons_of_sublist _: ?m.23784_ h: s <+ thGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ t·α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inr.intro.introa :: s <+ a :: t α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mp.inr.intro.introa :: s <+ a :: tα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = sexact h: s <+ th.cons_cons: ∀ {α : Type ?u.23794} {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → a :: l₁ <+ a :: l₂cons_cons _: ?m.23800_Goals accomplished! 🐙
α: Type uβ: Type vγ: Type ws, t: List αs ∈ sublists' t ↔ s <+ t·α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = scases' h: ?bh with _ _ _ h: s <+ th s: List ?m.23835s _ _ h: s <+ thα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = sα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s
α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s·α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = sα: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: sexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl h: s <+ thGoals accomplished! 🐙
α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ a :: tcons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s·α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s α: Type uβ: Type vγ: Type ws✝: List αa: αt: List αIH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ ts: List αh: s <+ tcons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: sexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr ⟨s: List ?m.23835s, h: s <+ th, rfl: ∀ {α : Sort ?u.24075} {a : α}, a = arfl⟩Goals accomplished! 🐙
#align list.mem_sublists' List.mem_sublists': ∀ {α : Type u} {s t : List α}, s ∈ sublists' t ↔ s <+ tList.mem_sublists'

@[simp]
theorem length_sublists': ∀ {α : Type u} (l : List α), length (sublists' l) = 2 ^ length llength_sublists' : ∀ l: List αl : List: Type ?u.24213 → Type ?u.24213List α: Type uα, length: {α : Type ?u.24217} → List α → ℕlength (sublists': {α : Type ?u.24219} → List α → List (List α)sublists' l: List αl) = 2: ?m.242282 ^ length: {α : Type ?u.24237} → List α → ℕlength l: List αl
| [] => rfl: ∀ {α : Sort ?u.24305} {a : α}, a = arfl
| a: αa :: l: List αl => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: αl: List αlength (sublists' (a :: l)) = 2 ^ length (a :: l)simp_arith only [sublists'_cons: ∀ {α : Type ?u.25753} (a : α) (l : List α), sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)sublists'_cons, length_append: ∀ {α : Type ?u.25766} (as bs : List α), length (as ++ bs) = length as + length bslength_append, length_sublists': ∀ (l : List α), length (sublists' l) = 2 ^ length llength_sublists' l: List αl,
length_map: ∀ {α : Type ?u.25785} {β : Type ?u.25784} (as : List α) (f : α → β), length (map f as) = length aslength_map, length: {α : Type ?u.25802} → List α → ℕlength, Nat.pow_succ': ∀ {m n : ℕ}, m ^ succ n = m * m ^ nNat.pow_succ', mul_succ: ∀ (n m : ℕ), n * succ m = n * m + nmul_succ, mul_zero: ∀ {M₀ : Type ?u.26088} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero, zero_add: ∀ {M : Type ?u.26105} [inst : AddZeroClass M] (a : M), 0 + a = azero_add]Goals accomplished! 🐙
#align list.length_sublists' List.length_sublists': ∀ {α : Type u} (l : List α), length (sublists' l) = 2 ^ length lList.length_sublists'

@[simp]
theorem sublists_nil: sublists [] = [[]]sublists_nil : sublists: {α : Type ?u.27870} → List α → List (List α)sublists (@nil: {α : Type ?u.27872} → List αnil α: Type uα) = [[]: List ?m.27878[]] :=
rfl: ∀ {α : Sort ?u.27910} {a : α}, a = arfl
#align list.sublists_nil List.sublists_nil: ∀ {α : Type u}, sublists [] = [[]]List.sublists_nil

@[simp]
theorem sublists_singleton: ∀ {α : Type u} (a : α), sublists [a] = [[], [a]]sublists_singleton (a: αa : α: Type uα) : sublists: {α : Type ?u.28569} → List α → List (List α)sublists [a: αa] = [[]: List ?m.28580[], [a: αa]] :=
rfl: ∀ {α : Sort ?u.28593} {a : α}, a = arfl
#align list.sublists_singleton List.sublists_singleton: ∀ {α : Type u} (a : α), sublists [a] = [[], [a]]List.sublists_singleton

--Porting note: Not the same as `sublists_aux` from Lean3
/-- Auxiliary helper function for `sublists` -/
def sublistsAux: α → List (List α) → List (List α)sublistsAux (a: αa : α: Type uα) (r: List (List α)r : List: Type ?u.40984 → Type ?u.40984List (List: Type ?u.40985 → Type ?u.40985List α: Type uα)) : List: Type ?u.40988 → Type ?u.40988List (List: Type ?u.40989 → Type ?u.40989List α: Type uα) :=
r: List (List α)r.foldl: {α : Type ?u.40994} → {β : Type ?u.40993} → (α → β → α) → α → List β → αfoldl (init := []: List ?m.41067[]) fun r: ?m.41006r l: ?m.41009l => r: ?m.41006r ++ [l: ?m.41009l, a: αa :: l: ?m.41009l]
#align list.sublists_aux List.sublistsAux: {α : Type u} → α → List (List α) → List (List α)List.sublistsAux

theorem sublistsAux_eq_array_foldl: sublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))sublistsAux_eq_array_foldl :
sublistsAux: {α : Type ?u.41178} → α → List (List α) → List (List α)sublistsAux = fun (a: αa : α: Type uα) (r: List (List α)r : List: Type ?u.41185 → Type ?u.41185List (List: Type ?u.41186 → Type ?u.41186List α: Type uα)) =>
(r: List (List α)r.toArray: {α : Type ?u.41188} → List α → Array αtoArray.foldl: {α : Type ?u.41192} →
{β : Type ?u.41191} → (β → α → β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ (Array.size as) → βfoldl (init := #[]: Array ?m.41221#[])
fun r: ?m.41208r l: ?m.41211l => (r: ?m.41208r.push: {α : Type ?u.41234} → Array α → α → Array αpush l: ?m.41211l).push: {α : Type ?u.41244} → Array α → α → Array αpush (a: αa :: l: ?m.41211l)).toList: {α : Type ?u.41228} → Array α → List αtoList := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wsublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))funext a: ?αa r: ?αrα: Type uβ: Type vγ: Type wa: αr: List (List α)h.hsublistsAux a r =   Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))
α: Type uβ: Type vγ: Type wsublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))simp only [sublistsAux: {α : Type ?u.41363} → α → List (List α) → List (List α)sublistsAux, Array.foldl_eq_foldl_data: ∀ {β : Type ?u.41365} {α : Type ?u.41366} (f : β → α → β) (init : β) (arr : Array α),
Array.foldl f init arr 0 (Array.size arr) = foldl f init arr.dataArray.foldl_eq_foldl_data, Array.mkEmpty: {α : Type ?u.41392} → ℕ → Array αArray.mkEmpty]α: Type uβ: Type vγ: Type wa: αr: List (List α)h.hfoldl (fun r l => r ++ [l, a :: l]) [] r =   Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
α: Type uβ: Type vγ: Type wsublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))have := foldl_hom: ∀ {α₁ : Type ?u.41564} {α₂ : Type ?u.41565} {β : Type ?u.41566} (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂)
(l : List β) (init : α₁), (∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)) → foldl g₂ (f init) l = f (foldl g₁ init l)foldl_hom Array.toList: {α : Type ?u.41570} → Array α → List αArray.toList (fun r: ?m.41576r l: ?m.41579l => (r: ?m.41576r.push: {α : Type ?u.41581} → Array α → α → Array αpush l: ?m.41579l).push: {α : Type ?u.41588} → Array α → α → Array αpush (a: ?αa :: l: ?m.41579l))
(fun (r: List (List α)r : List: Type ?u.41604 → Type ?u.41604List (List: Type ?u.41605 → Type ?u.41605List α: Type uα)) l: ?m.41608l => r: List (List α)r ++ [l: ?m.41608l, a: ?αa :: l: ?m.41608l]) r: ?αr #[]: Array ?m.41662#[]
(α: Type uβ: Type vγ: Type wa: αr: List (List α)h.hfoldl (fun r l => r ++ [l, a :: l]) [] r =   Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αr: List (List α)∀ (x : Array (List α)) (y : List α),
(fun r l => r ++ [l, a :: l]) (Array.toList x) y =     Array.toList ((fun r l => Array.push (Array.push r l) (a :: l)) x y)simpGoals accomplished! 🐙)α: Type uβ: Type vγ: Type wa: αr: List (List α)this: foldl (fun r l => r ++ [l, a :: l]) (Array.toList #[]) r =   Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] r)h.hfoldl (fun r l => r ++ [l, a :: l]) [] r =   Array.toList (foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r).data)
α: Type uβ: Type vγ: Type wsublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))simpa using this: ?m.41563thisGoals accomplished! 🐙

theorem sublistsAux_eq_bind: sublistsAux = fun a r => List.bind r fun l => [l, a :: l]sublistsAux_eq_bind :
sublistsAux: {α : Type ?u.44126} → α → List (List α) → List (List α)sublistsAux = fun (a: αa : α: Type uα) (r: List (List α)r : List: Type ?u.44133 → Type ?u.44133List (List: Type ?u.44134 → Type ?u.44134List α: Type uα)) => r: List (List α)r.bind: {α : Type ?u.44137} → {β : Type ?u.44136} → List α → (α → List β) → List βbind fun l: ?m.44146l => [l: ?m.44146l, a: αa :: l: ?m.44146l] :=
funext: ∀ {α : Sort ?u.44211} {β : α → Sort ?u.44210} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext <| fun a: ?m.44228a => funext: ∀ {α : Sort ?u.44231} {β : α → Sort ?u.44230} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext <| fun r: ?m.44243r =>
List.reverseRecOn: ∀ {α : Type ?u.44246} {C : List α → Sort ?u.44245} (l : List α),
C [] → (∀ (l : List α) (a : α), C l → C (l ++ [a])) → C lList.reverseRecOn r: ?m.44243r
(byGoals accomplished! 🐙 α: Type uβ: Type vγ: Type wa: αr: List (List α)sublistsAux a [] = List.bind [] fun l => [l, a :: l]simp [sublistsAux: {α : Type ?u.44296} → α → List (List α) → List (List α)sublistsAux]Goals accomplished! 🐙)
(fun r: ?m.44283r l: ?m.44286l ih: ?m.44289ih => byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wa: α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 [α: Type uβ: Type vγ: Type wa: α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]bind_append: ∀ {α : Type ?u.44529} {β : Type ?u.44528} (f : α → List β) (l₁ l₂ : List α),
List.bind (l₁ ++ l₂) f = List.bind l₁ f ++ List.bind l₂ fbind_append,α: Type uβ: Type vγ: Type wa: α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 fun l => [l, a :: l]) ++ List.bind [l] fun l => [l, a :: l] α: Type uβ: Type vγ: Type wa: α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]← ih: sublistsAux a r = List.bind r fun l => [l, a :: l]ih,α: Type uβ: Type vγ: Type wa: αr✝, r: List (List α)l: List αih: sublistsAux a r = List.bind r fun l => [l, a :: l]sublistsAux a (r ++ [l]) = sublistsAux a r ++ List.bind [l] fun l => [l, a :: l] α: Type uβ: Type vγ: Type wa: α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]bind_singleton: ∀ {α : Type ?u.44555} {β : Type ?u.44554} (f : α → List β) (x : α), List.bind [x] f = f xbind_singleton,α: Type uβ: Type vγ: Type wa: αr✝, r: List (List α)l: List αih: sublistsAux a r = List.bind r fun l => [l, a :: l]sublistsAux a (r ++ [l]) = sublistsAux a r ++ [l, a :: l] α: Type uβ: Type vγ: Type wa: α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]sublistsAux: {α : Type ?u.44584} → α → List (List α) → List (List α)sublistsAux,α: Type uβ: Type vγ: Type wa: α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]) [] (r ++ [l]) = sublistsAux a r ++ [l, a :: l] α: Type uβ: Type vγ: Type wa: α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]foldl_append: ∀ {α : Type ?u.44585} {β : Type ?u.44586} (f : β → α → β) (b : β) (l l' : List α),
foldl f b (l ++ l') = foldl f (foldl f b l) l'foldl_appendα: Type uβ: Type vγ: Type wa: α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 wa: α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 wa: α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]simp [sublistsAux: {α : Type ?u.44640} → α → List (List α) → List (List α)sublistsAux]Goals accomplished! 🐙)

theorem sublists_eq_sublistsAux: ∀ (l : List α), sublists l = foldr sublistsAux [[]] lsublists_eq_sublistsAux (l: List αl : List: Type ?u.44949 → Type ?u.44949List α: Type uα) :
sublists: {α : Type ?u.44953} → List α → List (List α)sublists l: List αl = l: List αl.foldr: {α : Type ?u.44958} → {β : Type ?u.44957} → (α → β → β) → β → List α → βfoldr sublistsAux: {α : Type ?u.44966} → α → List (List α) → List (List α)sublistsAux [[]: List ?m.44978[]] := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists l = foldr sublistsAux [[]] lsimp only [sublists: {α : Type ?u.44998} → List α → List (List α)sublists, sublistsAux_eq_array_foldl: ∀ {α : Type ?u.45000},
sublistsAux = fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r)))sublistsAux_eq_array_foldl, Array.foldr_eq_foldr_data: ∀ {α : Type ?u.45005} {β : Type ?u.45006} (f : α → β → β) (init : β) (arr : Array α),
Array.foldr f init arr (Array.size arr) = foldr f init arr.dataArray.foldr_eq_foldr_data]α: Type uβ: Type vγ: Type wl: List αArray.toList
(foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) (Array.mkEmpty (Array.size arr * 2)) arr 0
(Array.size arr))
#[[]] l) =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] l
α: Type uβ: Type vγ: Type wl: List αsublists l = foldr sublistsAux [[]] lrw [α: Type uβ: Type vγ: Type wl: List αArray.toList
(foldr
(fun a arr =>
Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) (Array.mkEmpty (Array.size arr * 2)) arr 0
(Array.size arr))
#[[]] l) =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] l← foldr_hom: ∀ {β₁ : Type ?u.45201} {β₂ : Type ?u.45202} {α : Type ?u.45203} (f : β₁ → β₂) (g₁ : α → β₁ → β₁) (g₂ : α → β₂ → β₂)
(l : List α) (init : β₁), (∀ (x : α) (y : β₁), g₂ x (f y) = f (g₁ x y)) → foldr g₂ (f init) l = f (foldr g₁ init l)foldr_hom Array.toList: {α : Type ?u.45207} → Array α → List αArray.toListα: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y))]α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y))
α: Type uβ: Type vγ: Type wl: List αsublists l = foldr sublistsAux [[]] l.α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] l α: Type uβ: Type vγ: Type wl: List αfoldr ?g₂ (Array.toList #[[]]) l =   foldr
(fun a r =>
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (a :: l)) #[] (toArray r) 0 (Array.size (toArray r))))
[[]] lα: Type uβ: Type vγ: Type wl: List αg₂α → List (List α) → List (List α)α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
?g₂ x (Array.toList y) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y))rflGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists l = foldr sublistsAux [[]] l.α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) #[] (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y)) α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) #[] (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y))intros _: ?m.45206_ _: Array ?m.45208_α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) #[] (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) (Array.mkEmpty (Array.size y✝ * 2)) y✝ 0
(Array.size y✝));α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) #[] (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) (Array.mkEmpty (Array.size y✝ * 2)) y✝ 0
(Array.size y✝)) α: Type uβ: Type vγ: Type wl: List αH∀ (x : α) (y : Array (List α)),
Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) #[] (toArray (Array.toList y)) 0
(Array.size (toArray (Array.toList y)))) =     Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x :: l)) (Array.mkEmpty (Array.size y * 2)) y 0
(Array.size y))congrα: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) #[] (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) (Array.mkEmpty (Array.size y✝ * 2)) y✝ 0
(Array.size y✝))<;>α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type uβ: Type vγ: Type wl: List αx✝: αy✝: Array (List α)HArray.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) #[] (toArray (Array.toList y✝)) 0
(Array.size (toArray (Array.toList y✝)))) =   Array.toList
(Array.foldl (fun r l => Array.push (Array.push r l) (x✝ :: l)) (Array.mkEmpty (Array.size y✝ * 2)) y✝ 0
(Array.size y✝))simpGoals accomplished! 🐙

#noalign list.sublists_aux₁_eq_sublists_aux
#noalign list.sublists_aux_cons_eq_sublists_aux₁
#noalign list.sublists_aux_eq_foldr.aux
#noalign list.sublists_aux_eq_foldr
#noalign list.sublists_aux_cons_cons
#noalign list.sublists_aux₁_append
#noalign list.sublists_aux₁_concat
#noalign list.sublists_aux₁_bind
#noalign list.sublists_aux_cons_append

theorem sublists_append: ∀ {α : Type u} (l₁ l₂ : List α),
sublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)sublists_append (l₁: List αl₁ l₂: List αl₂ : List: Type ?u.49191 → Type ?u.49191List α: Type uα) :
sublists: {α : Type ?u.49198} → List α → List (List α)sublists (l₁: List αl₁ ++ l₂: List αl₂) = (sublists: {α : Type ?u.49259} → List α → List (List α)sublists l₂: List αl₂) >>= (fun x: ?m.49264x => (sublists: {α : Type ?u.49266} → List α → List (List α)sublists l₁: List αl₁).map: {α : Type ?u.49270} → {β : Type ?u.49269} → (α → β) → List α → List βmap (. ++ x: ?m.49264x)) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl₁, l₂: List αsublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)simp only [sublists_eq_sublistsAux: ∀ {α : Type ?u.49350} (l : List α), sublists l = foldr sublistsAux [[]] lsublists_eq_sublistsAux, foldr_append: ∀ {α : Type ?u.49358} {β : Type ?u.49359} (f : α → β → β) (b : β) (l l' : List α),
foldr f b (l ++ l') = foldr f (foldr f b l') lfoldr_append, sublistsAux_eq_bind: ∀ {α : Type ?u.49387}, sublistsAux = fun a r => List.bind r fun l => [l, a :: l]sublistsAux_eq_bind]α: Type uβ: Type vγ: Type wl₁, l₂: List αfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)
α: Type uβ: Type vγ: Type wl₁, l₂: List αsublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)induction l₁: List αl₁α: Type uβ: Type vγ: Type wl₂: List αnilfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])α: Type uβ: Type vγ: Type wl₂: List αhead✝: αtail✝: List αtail_ih✝: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
tail✝ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] tail✝)consfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (head✝ :: tail✝))
α: Type uβ: Type vγ: Type wl₁, l₂: List αsublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁).α: Type uβ: Type vγ: Type wl₂: List αnilfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] []) α: Type uβ: Type vγ: Type wl₂: List αnilfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])α: Type uβ: Type vγ: Type wl₂: List αhead✝: αtail✝: List αtail_ih✝: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
tail✝ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] tail✝)consfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (head✝ :: tail✝))case nil => α: Type uβ: Type vγ: Type wl₂: List αfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) [] =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] [])simpGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl₁, l₂: List αsublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁).α: Type uβ: Type vγ: Type wl₂: List αhead✝: αtail✝: List αtail_ih✝: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
tail✝ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] tail✝)consfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (head✝ :: tail✝)) α: Type uβ: Type vγ: Type wl₂: List αhead✝: αtail✝: List αtail_ih✝: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
tail✝ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] tail✝)consfoldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (head✝ :: tail✝))case cons a: ?m.49645a l₁: List ?m.49645l₁ ih: ?m.49646 l₁ih =>
α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
(a :: l₁) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))rw [α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
(a :: l₁) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))foldr_cons: ∀ {α : Type ?u.50591} {β : Type ?u.50590} (f : α → β → β) (b : β) (a : α) (l : List α),
foldr f b (a :: l) = f a (foldr f b l)foldr_cons,α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)(List.bind
(foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
l₁)
fun l => [l, a :: l]) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁)) α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
(a :: l₁) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))ih: ?m.49646 l₁ihα: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)(List.bind
(do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁))
fun l => [l, a :: l]) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))]α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)(List.bind
(do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁))
fun l => [l, a :: l]) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))
α: Type uβ: Type vγ: Type wl₂: List αa: αl₁: List αih: foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂) l₁ =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₁)foldr (fun a r => List.bind r fun l => [l, a :: l]) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂)
(a :: l₁) =   do
let x ← foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] l₂
map (fun x_1 => x_1 ++ x) (foldr (fun a r => List.bind r fun l => [l, a :: l]) [[]] (a :: l₁))simp [List.bind: {α : Type ?u.50643} → {β : Type ?u.50642} → List α → (α → List β) → List βList.bind, join_join: ∀ {α : Type ?u.50645} (l : List (List (List α))), join (join l) = join (map join l)join_join, Function.comp: {α : Sort ?u.50655} → {β : Sort ?u.50654} → {δ : Sort ?u.50653} → (β → δ) → (α → β) → α → δFunction.comp]Goals accomplished! 🐙
#align list.sublists_append List.sublists_append: ∀ {α : Type u} (l₁ l₂ : List α),
sublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)List.sublists_append

--Portin note: New theorem
theorem sublists_cons: ∀ (a : α) (l : List α),
sublists (a :: l) = do
let x ← sublists l
[x, a :: x]sublists_cons (a: αa : α: Type uα) (l: List αl : List: Type ?u.59461 → Type ?u.59461List α: Type uα) :
sublists: {α : Type ?u.59465} → List α → List (List α)sublists (a: αa :: l: List αl) = sublists: {α : Type ?u.59477} → List α → List (List α)sublists l: List αl >>= (fun x: ?m.59482x => [x: ?m.59482x, a: αa :: x: ?m.59482x]) :=
show sublists: {α : Type ?u.59516} → List α → List (List α)sublists ([a: αa] ++ l: List αl) = _: ?m.59575_ by
rw [α: Type uβ: Type vγ: Type wa: αl: List αsublists ([a] ++ l) = do
let x ← sublists l
[x, a :: x]sublists_append: ∀ {α : Type ?u.59614} (l₁ l₂ : List α),
sublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)sublists_appendα: Type uβ: Type vγ: Type wa: αl: List α(do
let x ← sublists l
map (fun x_1 => x_1 ++ x) (sublists [a])) =   do
let x ← sublists l
[x, a :: x]]α: Type uβ: Type vγ: Type wa: αl: List α(do
let x ← sublists l
map (fun x_1 => x_1 ++ x) (sublists [a])) =   do
let x ← sublists l
[x, a :: x]
α: Type uβ: Type vγ: Type wa: αl: List αsublists ([a] ++ l) = do
let x ← sublists l
[x, a :: x]simp only [sublists_singleton: ∀ {α : Type ?u.59669} (a : α), sublists [a] = [[], [a]]sublists_singleton, map_cons: ∀ {α : Type ?u.59679} {β : Type ?u.59680} (f : α → β) (a : α) (l : List α), map f (a :: l) = f a :: map f lmap_cons, bind_eq_bind: ∀ {α β : Type ?u.59700} (f : α → List β) (l : List α), l >>= f = List.bind l fbind_eq_bind, nil_append: ∀ {α : Type ?u.59718} (as : List α), [] ++ as = asnil_append, cons_append: ∀ {α : Type ?u.59725} (a : α) (as bs : List α), a :: as ++ bs = a :: (as ++ bs)cons_append, map_nil: ∀ {α : Type ?u.59735} {β : Type ?u.59736} {f : α → β}, map f [] = []map_nil]Goals accomplished! 🐙

@[simp]
theorem sublists_concat: ∀ {α : Type u} (l : List α) (a : α), sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)sublists_concat (l: List αl : List: Type ?u.59968 → Type ?u.59968List α: Type uα) (a: αa : α: Type uα) :
sublists: {α : Type ?u.59974} → List α → List (List α)sublists (l: List αl ++ [a: αa]) = sublists: {α : Type ?u.60036} → List α → List (List α)sublists l: List αl ++ map: {α : Type ?u.60040} → {β : Type ?u.60039} → (α → β) → List α → List βmap (fun x: ?m.60044x => x: ?m.60044x ++ [a: αa]) (sublists: {α : Type ?u.60085} → List α → List (List α)sublists l: List αl) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)rw [α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)sublists_append: ∀ {α : Type ?u.60120} (l₁ l₂ : List α),
sublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)sublists_append,α: Type uβ: Type vγ: Type wl: List αa: α(do
let x ← sublists [a]
map (fun x_1 => x_1 ++ x) (sublists l)) =   sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)sublists_singleton: ∀ {α : Type ?u.60140} (a : α), sublists [a] = [[], [a]]sublists_singleton,α: Type uβ: Type vγ: Type wl: List αa: α(do
let x ← [[], [a]]
map (fun x_1 => x_1 ++ x) (sublists l)) =   sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)bind_eq_bind: ∀ {α β : Type ?u.60155} (f : α → List β) (l : List α), l >>= f = List.bind l fbind_eq_bind,α: Type uβ: Type vγ: Type wl: List αa: α(List.bind [[], [a]] fun x => map (fun x_1 => x_1 ++ x) (sublists l)) =   sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)cons_bind: ∀ {α : Type ?u.60178} {β : Type ?u.60179} (x : α) (xs : List α) (f : α → List β),
List.bind (x :: xs) f = f x ++ List.bind xs fcons_bind,α: Type uβ: Type vγ: Type wl: List αa: α(map (fun x => x ++ []) (sublists l) ++ List.bind [[a]] fun x => map (fun x_1 => x_1 ++ x) (sublists l)) =   sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)cons_bind: ∀ {α : Type ?u.60201} {β : Type ?u.60202} (x : α) (xs : List α) (f : α → List β),
List.bind (x :: xs) f = f x ++ List.bind xs fcons_bind,α: Type uβ: Type vγ: Type wl: List αa: αmap (fun x => x ++ []) (sublists l) ++     (map (fun x => x ++ [a]) (sublists l) ++ List.bind [] fun x => map (fun x_1 => x_1 ++ x) (sublists l)) =   sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)nil_bind: ∀ {α : Type ?u.60221} {β : Type ?u.60222} (f : α → List β), List.bind [] f = []nil_bind,α: Type uβ: Type vγ: Type wl: List αa: αmap (fun x => x ++ []) (sublists l) ++ (map (fun x => x ++ [a]) (sublists l) ++ []) =   sublists l ++ map (fun x => x ++ [a]) (sublists l)
α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)map_id': ∀ {α : Type ?u.60239} {f : α → α}, (∀ (x : α), f x = x) → ∀ (l : List α), map f l = lmap_id' append_nil: ∀ {α : Type ?u.60242} (as : List α), as ++ [] = asappend_nil,α: Type uβ: Type vγ: Type wl: List αa: αsublists l ++ (map (fun x => x ++ [a]) (sublists l) ++ []) = sublists l ++ map (fun x => x ++ [a]) (sublists l) α: Type uβ: Type vγ: Type wl: List αa: αsublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)append_nil: ∀ {α : Type ?u.60269} (as : List α), as ++ [] = asappend_nilα: Type uβ: Type vγ: Type wl: List αa: αsublists l ++ map (fun x => x ++ [a]) (sublists l) = sublists l ++ map (fun x => x ++ [a]) (sublists l)]Goals accomplished! 🐙
#align list.sublists_concat List.sublists_concat: ∀ {α : Type u} (l : List α) (a : α), sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)List.sublists_concat

theorem sublists_reverse: ∀ (l : List α), sublists (reverse l) = map reverse (sublists' l)sublists_reverse (l: List αl : List: Type ?u.60340 → Type ?u.60340List α: Type uα) : sublists: {α : Type ?u.60344} → List α → List (List α)sublists (reverse: {α : Type ?u.60346} → List α → List αreverse l: List αl) = map: {α : Type ?u.60352} → {β : Type ?u.60351} → (α → β) → List α → List βmap reverse: {α : Type ?u.60355} → List α → List αreverse (sublists': {α : Type ?u.60360} → List α → List (List α)sublists' l: List αl) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists (reverse l) = map reverse (sublists' l)induction' l: List αl with hd: ?m.60387hd tl: List ?m.60387tl ih: ?m.60388 tlihα: Type uβ: Type vγ: Type wnilsublists (reverse []) = map reverse (sublists' [])α: Type uβ: Type vγ: Type whd: αtl: List αih: sublists (reverse tl) = map reverse (sublists' tl)conssublists (reverse (hd :: tl)) = map reverse (sublists' (hd :: tl)) <;> [α: Type uβ: Type vγ: Type wl: List αsublists (reverse l) = map reverse (sublists' l)rflGoals accomplished! 🐙;
α: Type uβ: Type vγ: Type wl: List αsublists (reverse l) = map reverse (sublists' l)simp only [reverse_cons: ∀ {α : Type ?u.61426} (a : α) (as : List α), reverse (a :: as) = reverse as ++ [a]reverse_cons, sublists_append: ∀ {α : Type ?u.61439} (l₁ l₂ : List α),
sublists (l₁ ++ l₂) = do
let x ← sublists l₂
map (fun x_1 => x_1 ++ x) (sublists l₁)sublists_append, sublists'_cons: ∀ {α : Type ?u.61456} (a : α) (l : List α), sublists' (a :: l) = sublists' l ++ map (cons a) (sublists' l)sublists'_cons, map_append: ∀ {α : Type ?u.61466} {β : Type ?u.61467} (f : α → β) (l₁ l₂ : List α), map f (l₁ ++ l₂) = map f l₁ ++ map f l₂map_append, ih: ?m.60388 tlih, sublists_singleton: ∀ {α : Type ?u.61492} (a : α), sublists [a] = [[], [a]]sublists_singleton,
map_eq_map: ∀ {α β : Type ?u.61499} (f : α → β) (l : List α), f <\$> l = map f lmap_eq_map, bind_eq_bind: ∀ {α β : Type ?u.61517} (f : α → List β) (l : List α), l >>= f = List.bind l fbind_eq_bind, map_map: ∀ {β : Type ?u.61535} {γ : Type ?u.61536} {α : Type ?u.61537} (g : β → γ) (f : α → β) (l : List α),
map g (map f l) = map (g ∘ f) lmap_map, cons_bind: ∀ {α : Type ?u.61556} {β : Type ?u.61557} (x : α) (xs : List α) (f : α → List β),
List.bind (x :: xs) f = f x ++ List.bind xs fcons_bind, append_nil: ∀ {α : Type ?u.61577} (as : List α), as ++ [] = asappend_nil, nil_bind: ∀ {α : Type ?u.61583} {β : Type ?u.61584} (f : α → List β), List.bind [] f = []nil_bind, (· ∘ ·)]Goals accomplished! 🐙]Goals accomplished! 🐙
#align list.sublists_reverse List.sublists_reverse: ∀ {α : Type u} (l : List α), sublists (reverse l) = map reverse (sublists' l)List.sublists_reverse

theorem sublists_eq_sublists': ∀ (l : List α), sublists l = map reverse (sublists' (reverse l))sublists_eq_sublists' (l: List αl : List: Type ?u.62000 → Type ?u.62000List α: Type uα) : sublists: {α : Type ?u.62004} → List α → List (List α)sublists l: List αl = map: {α : Type ?u.62009} → {β : Type ?u.62008} → (α → β) → List α → List βmap reverse: {α : Type ?u.62012} → List α → List αreverse (sublists': {α : Type ?u.62017} → List α → List (List α)sublists' (reverse: {α : Type ?u.62020} → List α → List αreverse l: List αl)) := byGoals accomplished! 🐙
α: Type uβ: Type vγ: Type wl: List αsublists l = map reverse (sublists' (reverse l))rw [α: Type uβ: Type vγ: Type wl: List αsublists l = map reverse (sublists' (reverse l))← sublists_reverse: ∀ {α : Type ?u.62029} (l : List α), sublists (reverse l) = map reverse (sublists' l)sublists_reverse,α: Type uβ: Type vγ: Type wl: List αsublists l = sublists (reverse (reverse l)) α: Type uβ: Type vγ: Type wl: List αsublists l = map reverse (sublists' (reverse l))reverse_reverse: ∀ {α : Type ?u.62045} (as : List α), reverse (reverse as) = asreverse_reverseα: Type uβ: Type vγ: Type wl: List αsublists l = sublists l]Goals accomplished! 🐙
#align list.sublists_eq_sublists' List.sublists_eq_sublists': ∀ {α : Type u} (l : List α), sublists l = map reverse (sublists' (reverse l))List.sublists_eq_sublists'

theorem sublists'_reverse: ∀ {α : Type u} (l : List α), sublists' (reverse l) = map reverse (sublists l)sublists'_reverse (l: List αl : List: Type ?u.62069 → Type ?u.62069List α: Type uα) : sublists': {α : Type ?u.62073} → List α → List (List α)sublists' (reverse: {α : Type ?u.62075} → List α → List αreverse```