/-
Copyright (c) 2019 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.list.sublists
! leanprover-community/mathlib commit ccad6d5093bd2f5c6ca621fc74674cce51355af6
! 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 = a
rfl
#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 = a
rfl
#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.13573
List (List: Type ?u.13574 → Type ?u.13574
List α: Type u
α)) : List: Type ?u.13581 → Type ?u.13581
List (List: Type ?u.13582 → Type ?u.13582
List α: Type u
α) :=
  r₁: List (List α)
r₁.foldl: {α : Type ?u.13588} → {β : Type ?u.13587} → (α → β → α) → α → List β → α
foldl (init := r₂: List (List α)
r₂) fun r: ?m.13600
r l: ?m.13603
l => r: ?m.13600
r ++ [a: α
a :: l: ?m.13603
l]
#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.13796
List (List: Type ?u.13797 → Type ?u.13797
List α: 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.13825
r l: ?m.13828
l => r: ?m.13825
r.push: {α : Type ?u.13843} → Array α → α → Array α
push (a: α
a :: l: ?m.13828
l))).toList: {α : Type ?u.13839} → Array α → List α
toList := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

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₁)))intro r₁: List (List α)
r₁ r₂: List (List α)
r₂α: Type u

β: Type v

γ: Type w

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₁)))
  α: Type u

β: Type v

γ: Type w

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₁)))rw [α: Type u

β: Type v

γ: Type w

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: {α : Type ?u.13888} → α → List (List α) → List (List α) → List (List α)
sublists'Aux,α: Type u

β: Type v

γ: Type w

a: α

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 w

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₁)))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.data
Array.foldl_eq_foldl_dataα: Type u

β: Type v

γ: Type w

a: α

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 w

a: α

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 w

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₁)))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.13957
r l: ?m.13960
l => r: ?m.13957
r.push: {α : Type ?u.13962} → Array α → α → Array α
push (a: α
a :: l: ?m.13960
l))
    (fun r: ?m.13978
r l: ?m.13981
l => r: ?m.13978
r ++ [a: α
a :: l: ?m.13981
l]) r₁: List (List α)
r₁ r₂: List (List α)
r₂.toArray: {α : Type ?u.14032} → List α → Array α
toArray (α: Type u

β: Type v

γ: Type w

a: α

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)by
Goals accomplished! 🐙 α: Type u

β: Type v

γ: Type w

a: α

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)simp
Goals accomplished! 🐙)α: Type u

β: Type v

γ: Type w

a: α

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 w

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₁)))simpa using this: ?m.13944
this
Goals accomplished! 🐙

theorem sublists'_eq_sublists'Aux: ∀ (l : List α), sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l
sublists'_eq_sublists'Aux (l: List α
l : List: Type ?u.16547 → Type ?u.16547
List α: 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.16565
a r: ?m.16568
r => sublists'Aux: {α : Type ?u.16570} → α → List (List α) → List (List α) → List (List α)
sublists'Aux a: ?m.16565
a r: ?m.16568
r r: ?m.16568
r) [[]: List ?m.16581
[]] := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] ldsimp onlyα: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] lrw [α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l.α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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))rfl
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: List α

sublists' l = foldr (fun a r => sublists'Aux a r r) [[]] l.α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: 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 w

l: 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 w

l: 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 w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_4.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_4.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type u

β: Type v

γ: Type w

l: 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✝))simp
Goals 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.20930
List (List: Type ?u.20931 → Type ?u.20931
List α: Type u
α)) : ∀ (r₂: List (List α)
r₂ : List: Type ?u.20935 → Type ?u.20935
List (List: Type ?u.20936 → Type ?u.20936
List α: 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 l
List.reverseRecOn r₁: List (List α)
r₁ (fun _: ?m.21029
_ => by
Goals accomplished! 🐙 α: Type u

β: Type v

γ: Type w

a: α

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.21035
r₁ l: ?m.21038
l ih: ?m.21041
ih r₂: ?m.21045
r₂ => by
Goals accomplished! 🐙
    α: Type u

β: Type v

γ: Type w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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.22065
List α: 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) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

a: α

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) [[]] l
sublists'_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 <+ t
mem_sublists' {s: List α
s t: List α
t : List: Type ?u.23106 → Type ?u.23106
List α: Type u
α} : s: List α
s ∈ sublists': {α : Type ?u.23115} → List α → List (List α)
sublists' t: List α
t ↔ s: List α
s <+ t: List α
t := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ tinduction' t: List α
t with a: ?m.23154
a t: List ?m.23154
t IH: ?m.23155 t
IH generalizing s: List α
sα: Type u

β: Type v

γ: Type w

s✝, s: List α

nils ∈ sublists' [] ↔ s <+ []
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

conss ∈ sublists' (a :: t) ↔ s <+ a :: t
  α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ t·α: Type u

β: Type v

γ: Type w

s✝, s: List α

nils ∈ sublists' [] ↔ s <+ [] α: Type u

β: Type v

γ: Type w

s✝, s: List α

nils ∈ sublists' [] ↔ s <+ []
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: 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 = b
mem_singleton]α: Type u

β: Type v

γ: Type w

s✝, s: List α

nils = [] ↔ s <+ []
    α: Type u

β: Type v

γ: Type w

s✝, s: List α

nils ∈ sublists' [] ↔ s <+ []exact ⟨fun h: ?m.23316
h => α: Type u

β: Type v

γ: Type w

s✝, s: List α

nils = [] ↔ s <+ []by
Goals accomplished! 🐙 α: Type u

β: Type v

γ: Type w

s✝, s: List α

h: s = []

s <+ []rw [α: Type u

β: Type v

γ: Type w

s✝, s: List α

h: s = []

s <+ []h: s = []
hα: Type u

β: Type v

γ: Type w

s✝, 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 w

s, 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 ∈ t
mem_append, IH: ?m.23155 t
IH, mem_map: ∀ {α : Type ?u.23411} {β : Type ?u.23412} {b : β} {f : α → β} {l : List α}, b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b
mem_map]α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
  α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ tconstructorα: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons.mp(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons.mprs <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t<;>α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons.mp(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons.mprs <+ a :: t → s <+ t ∨ ∃ a_2, a_2 <+ t ∧ a :: a_2 = s α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

cons(s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: tintro h: ?a
hα: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s;α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s

cons.mps <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ trcases h: ?a
h with (h | ⟨s, h, rfl⟩): ?a
(h: s <+ t
hh | ⟨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 <+ t
h⟨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 w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inls <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inr.intro.introa :: s <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
  α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ t·α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inls <+ a :: t α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inls <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inr.intro.introa :: s <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.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 <+ t
h
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

s, t: List α

s ∈ sublists' t ↔ s <+ t·α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inr.intro.introa :: s <+ a :: t α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mp.inr.intro.introa :: s <+ a :: t
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = sexact h: s <+ t
h.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 w

s, t: List α

s ∈ sublists' t ↔ s <+ t·α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = scases' h: ?b
h with _ _ _ h: s <+ t
h s: List ?m.23835
s _ _ h: s <+ t
hα: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s
    α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s·α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.conss <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: sexact Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl h: s <+ t
h
Goals accomplished! 🐙
    α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ a :: t

cons.mprs <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s·α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: s α: Type u

β: Type v

γ: Type w

s✝: List α

a: α

t: List α

IH: ∀ {s : List α}, s ∈ sublists' t ↔ s <+ t

s: List α

h: s <+ t

cons.mpr.cons₂a :: s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = a :: sexact Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr ⟨s: List ?m.23835
s, h: s <+ t
h, rfl: ∀ {α : Sort ?u.24075} {a : α}, a = a
rfl⟩
Goals accomplished! 🐙
#align list.mem_sublists' List.mem_sublists': ∀ {α : Type u} {s t : List α}, s ∈ sublists' t ↔ s <+ t
List.mem_sublists'

@[simp]
theorem length_sublists': ∀ {α : Type u} (l : List α), length (sublists' l) = 2 ^ length l
length_sublists' : ∀ l: List α
l : List: Type ?u.24213 → Type ?u.24213
List α: Type u
α, length: {α : Type ?u.24217} → List α → ℕ
length (sublists': {α : Type ?u.24219} → List α → List (List α)
sublists' l: List α
l) = 2: ?m.24228
2 ^ length: {α : Type ?u.24237} → List α → ℕ
length l: List α
l
  | [] => rfl: ∀ {α : Sort ?u.24305} {a : α}, a = a
rfl
  | a: α
a :: l: List α
l => by
Goals accomplished! 🐙
    α: Type u

β: Type v

γ: Type w

a: α

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 bs
length_append, length_sublists': ∀ (l : List α), length (sublists' l) = 2 ^ length l
length_sublists' l: List α
l,
      length_map: ∀ {α : Type ?u.25785} {β : Type ?u.25784} (as : List α) (f : α → β), length (map f as) = length as
length_map, length: {α : Type ?u.25802} → List α → ℕ
length, Nat.pow_succ': ∀ {m n : ℕ}, m ^ succ n = m * m ^ n
Nat.pow_succ', mul_succ: ∀ (n m : ℕ), n * succ m = n * m + n
mul_succ, mul_zero: ∀ {M₀ : Type ?u.26088} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero, zero_add: ∀ {M : Type ?u.26105} [inst : AddZeroClass M] (a : M), 0 + a = a
zero_add]
Goals accomplished! 🐙
#align list.length_sublists' List.length_sublists': ∀ {α : Type u} (l : List α), length (sublists' l) = 2 ^ length l
List.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 = a
rfl
#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 = a
rfl
#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.40984
List (List: Type ?u.40985 → Type ?u.40985
List α: Type u
α)) : List: Type ?u.40988 → Type ?u.40988
List (List: Type ?u.40989 → Type ?u.40989
List α: Type u
α) :=
  r: List (List α)
r.foldl: {α : Type ?u.40994} → {β : Type ?u.40993} → (α → β → α) → α → List β → α
foldl (init := []: List ?m.41067
[]) fun r: ?m.41006
r l: ?m.41009
l => r: ?m.41006
r ++ [l: ?m.41009
l, a: α
a :: l: ?m.41009
l]
#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.41185
List (List: Type ?u.41186 → Type ?u.41186
List α: 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.41208
r l: ?m.41211
l => (r: ?m.41208
r.push: {α : Type ?u.41234} → Array α → α → Array α
push l: ?m.41211
l).push: {α : Type ?u.41244} → Array α → α → Array α
push (a: α
a :: l: ?m.41211
l)).toList: {α : Type ?u.41228} → Array α → List α
toList := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

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)))funext a: ?α
a r: ?α
rα: Type u

β: Type v

γ: Type w

a: α

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 w

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)))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.data
Array.foldl_eq_foldl_data, Array.mkEmpty: {α : Type ?u.41392} → ℕ → Array α
Array.mkEmpty]α: Type u

β: Type v

γ: Type w

a: α

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 w

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)))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.41576
r l: ?m.41579
l => (r: ?m.41576
r.push: {α : Type ?u.41581} → Array α → α → Array α
push l: ?m.41579
l).push: {α : Type ?u.41588} → Array α → α → Array α
push (a: ?α
a :: l: ?m.41579
l))
    (fun (r: List (List α)
r : List: Type ?u.41604 → Type ?u.41604
List (List: Type ?u.41605 → Type ?u.41605
List α: Type u
α)) l: ?m.41608
l => r: List (List α)
r ++ [l: ?m.41608
l, a: ?α
a :: l: ?m.41608
l]) r: ?α
r #[]: Array ?m.41662
#[]
    (α: Type u

β: Type v

γ: Type w

a: α

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)by
Goals accomplished! 🐙 α: Type u

β: Type v

γ: Type w

a: α

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)simp
Goals accomplished! 🐙)α: Type u

β: Type v

γ: Type w

a: α

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 w

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)))simpa using this: ?m.41563
this
Goals 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.44133
List (List: Type ?u.44134 → Type ?u.44134
List α: Type u
α)) => r: List (List α)
r.bind: {α : Type ?u.44137} → {β : Type ?u.44136} → List α → (α → List β) → List β
bind fun l: ?m.44146
l => [l: ?m.44146
l, a: α
a :: l: ?m.44146
l] :=
  funext: ∀ {α : Sort ?u.44211} {β : α → Sort ?u.44210} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext <| fun a: ?m.44228
a => funext: ∀ {α : Sort ?u.44231} {β : α → Sort ?u.44230} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext <| fun r: ?m.44243
r =>
  List.reverseRecOn: ∀ {α : Type ?u.44246} {C : List α → Sort ?u.44245} (l : List α),
  C [] → (∀ (l : List α) (a : α), C l → C (l ++ [a])) → C l
List.reverseRecOn r: ?m.44243
r
    (by
Goals accomplished! 🐙 α: Type u

β: Type v

γ: Type w

a: α

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.44283
r l: ?m.44286
l ih: ?m.44289
ih => by
Goals accomplished! 🐙
      α: 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 [α: 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]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₂ f
bind_append,α: 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 fun l => [l, a :: l]) ++ List.bind [l] fun l => [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]← ih: sublistsAux a r = List.bind r fun l => [l, a :: l]
ih,α: 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]) = sublistsAux a r ++ List.bind [l] fun l => [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]bind_singleton: ∀ {α : Type ?u.44555} {β : Type ?u.44554} (f : α → List β) (x : α), List.bind [x] f = f x
bind_singleton,α: 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]) = 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]sublistsAux: {α : Type ?u.44584} → α → List (List α) → List (List α)
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]) [] (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]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 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]

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]simp [sublistsAux: {α : Type ?u.44640} → α → List (List α) → List (List α)
sublistsAux]
Goals accomplished! 🐙)

theorem sublists_eq_sublistsAux: ∀ (l : List α), sublists l = foldr sublistsAux [[]] l
sublists_eq_sublistsAux (l: List α
l : List: Type ?u.44949 → Type ?u.44949
List α: 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
[]] := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: 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.data
Array.foldr_eq_foldr_data]α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

sublists l = foldr sublistsAux [[]] lrw [α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

sublists l = foldr sublistsAux [[]] l.α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: List α

g₂α → List (List α) → List (List α)
α: Type u

β: Type v

γ: Type w

l: 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))rfl
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: List α

sublists l = foldr sublistsAux [[]] l.α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: 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 w

l: 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 w

l: 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 w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_5.htoArray (Array.toList y✝) = y✝
α: Type u

β: Type v

γ: Type w

l: List α

x✝: α

y✝: Array (List α)

H.e_as.h.e_7.e_atoArray (Array.toList y✝) = y✝ α: Type u

β: Type v

γ: Type w

l: 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✝))simp
Goals 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.49191
List α: 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.49264
x => (sublists: {α : Type ?u.49266} → List α → List (List α)
sublists l₁: List α
l₁).map: {α : Type ?u.49270} → {β : Type ?u.49269} → (α → β) → List α → List β
map (. ++ x: ?m.49264
x)) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l₁, 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 [[]] l
sublists_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') l
foldr_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 w

l₁, 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 w

l₁, 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 w

l₂: 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 w

l₂: 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₂)
    (head✝ :: 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]) [[]] (head✝ :: tail✝))
  α: Type u

β: Type v

γ: Type w

l₁, l₂: List α

sublists (l₁ ++ l₂) = do
  let x ← sublists l₂
  map (fun x_1 => x_1 ++ x) (sublists l₁).α: Type u

β: Type v

γ: Type w

l₂: 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 w

l₂: 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 w

l₂: 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₂)
    (head✝ :: 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]) [[]] (head✝ :: tail✝))case nil => α: Type u

β: Type v

γ: Type w

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₂) [] =   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]) [[]] [])simp
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l₁, l₂: List α

sublists (l₁ ++ l₂) = do
  let x ← sublists l₂
  map (fun x_1 => x_1 ++ x) (sublists l₁).α: Type u

β: Type v

γ: Type w

l₂: 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₂)
    (head✝ :: 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]) [[]] (head✝ :: tail✝)) α: Type u

β: Type v

γ: Type w

l₂: 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₂)
    (head✝ :: 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]) [[]] (head✝ :: tail✝))case cons a: ?m.49645
a l₁: List ?m.49645
l₁ ih: ?m.49646 l₁
ih =>
      α: Type u

β: Type v

γ: Type w

l₂: 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 w

l₂: 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 w

l₂: 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 w

l₂: 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 w

l₂: 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 w

l₂: 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 w

l₂: 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.59461
List α: 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.59482
x => [x: ?m.59482
x, a: α
a :: x: ?m.59482
x]) :=
  show sublists: {α : Type ?u.59516} → List α → List (List α)
sublists ([a: α
a] ++ l: List α
l) = _: ?m.59575
_ by
  rw [α: Type u

β: Type v

γ: Type w

a: α

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 w

a: α

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 w

a: α

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 w

a: α

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 l
map_cons, bind_eq_bind: ∀ {α β : Type ?u.59700} (f : α → List β) (l : List α), l >>= f = List.bind l f
bind_eq_bind, nil_append: ∀ {α : Type ?u.59718} (as : List α), [] ++ as = as
nil_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.59968
List α: 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.60044
x => x: ?m.60044
x ++ [a: α
a]) (sublists: {α : Type ?u.60085} → List α → List (List α)
sublists l: List α
l) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: List α

a: α

sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)rw [α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: 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 w

l: 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 w

l: 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 f
bind_eq_bind,α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 f
cons_bind,α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 f
cons_bind,α: Type u

β: Type v

γ: Type w

l: 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 w

l: 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 w

l: 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 w

l: 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 = l
map_id' append_nil: ∀ {α : Type ?u.60242} (as : List α), as ++ [] = as
append_nil,α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

a: α

sublists (l ++ [a]) = sublists l ++ map (fun x => x ++ [a]) (sublists l)append_nil: ∀ {α : Type ?u.60269} (as : List α), as ++ [] = as
append_nilα: Type u

β: Type v

γ: Type w

l: 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.60340
List α: 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) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: List α

sublists (reverse l) = map reverse (sublists' l)induction' l: List α
l with hd: ?m.60387
hd tl: List ?m.60387
tl ih: ?m.60388 tl
ihα: Type u

β: Type v

γ: Type w

nilsublists (reverse []) = map reverse (sublists' [])
α: Type u

β: Type v

γ: Type w

hd: α

tl: List α

ih: sublists (reverse tl) = map reverse (sublists' tl)

conssublists (reverse (hd :: tl)) = map reverse (sublists' (hd :: tl)) <;> [α: Type u

β: Type v

γ: Type w

l: List α

sublists (reverse l) = map reverse (sublists' l)rfl
Goals accomplished! 🐙;
    α: Type u

β: Type v

γ: Type w

l: 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 tl
ih, sublists_singleton: ∀ {α : Type ?u.61492} (a : α), sublists [a] = [[], [a]]
sublists_singleton,
      map_eq_map: ∀ {α β : Type ?u.61499} (f : α → β) (l : List α), f <$> l = map f l
map_eq_map, bind_eq_bind: ∀ {α β : Type ?u.61517} (f : α → List β) (l : List α), l >>= f = List.bind l f
bind_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) l
map_map, cons_bind: ∀ {α : Type ?u.61556} {β : Type ?u.61557} (x : α) (xs : List α) (f : α → List β),
  List.bind (x :: xs) f = f x ++ List.bind xs f
cons_bind, append_nil: ∀ {α : Type ?u.61577} (as : List α), as ++ [] = as
append_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.62000
List α: 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)) := by
Goals accomplished! 🐙
  α: Type u

β: Type v

γ: Type w

l: List α

sublists l = map reverse (sublists' (reverse l))rw [α: Type u

β: Type v

γ: Type w

l: 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 w

l: List α

sublists l = sublists (reverse (reverse l)) α: Type u

β: Type v

γ: Type w

l: List α

sublists l = map reverse (sublists' (reverse l))reverse_reverse: ∀ {α : Type ?u.62045} (as : List α), reverse (reverse as) = as
reverse_reverseα: Type u

β: Type v

γ: Type w

l: 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.62069
List α: Type u
α) : sublists': {α : Type ?u.62073} → List α → List (List α)
sublists' (reverse: {α : Type ?u.62075} → List α → List α
reverse