-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem sections_eq_sectionsTR : @sections = @sectionsTR

Proof state:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ flatMap (fun s => map (fun a => a :: s) l) (foldr sectionsTR.go #[[]] L).toList =
    #[].toList ++ flatMap ?h.h.false.cons.G (foldr sectionsTR.go #[[]] L).toList

case h.h.false.cons.G
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ List α → List (List α)

case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => acc'.push (a_1 :: a)) acc l).toList = acc.toList ++ ?h.h.false.cons.G a

Tactic:
rfl

Result:
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => acc'.push (a_1 :: a)) acc l).toList = acc.toList ++ map (fun a_1 => a_1 :: a) l

Proof state:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ (l :: L).sections = (foldr sectionsTR.go #[[]] (l :: L)).toList

Tactic:
simp [IH, sectionsTR.go]

Result:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ flatMap (fun s => map (fun a => a :: s) l) (foldr sectionsTR.go #[[]] L).toList =
    (Array.foldl (fun acc' l' => foldl (fun acc' a => acc'.push (a :: l')) acc' l) #[]
        (foldr sectionsTR.go #[[]] L)).toList

Proof state:
case h.h.false
α : Type u_1
L : List (List α)
⊢ L.sections = (foldr sectionsTR.go #[[]] L).toList

Tactic:
induction L with | nil => rfl | cons l L IH => ?_

Result:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ (l :: L).sections = (foldr sectionsTR.go #[[]] (l :: L)).toList

Proof state:
case h.h.false.nil
α : Type u_1
⊢ [].sections = (foldr sectionsTR.go #[[]] []).toList

Tactic:
rfl

Result:
no goals

Proof state:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ flatMap (fun s => map (fun a => a :: s) l) (foldr sectionsTR.go #[[]] L).toList =
    (Array.foldl (fun acc' l' => foldl (fun acc' a => acc'.push (a :: l')) acc' l) #[]
        (foldr sectionsTR.go #[[]] L)).toList

Tactic:
rw [← Array.foldl_toList, Array.foldl_toList_eq_flatMap]

Result:
case h.h.false.cons
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ flatMap (fun s => map (fun a => a :: s) l) (foldr sectionsTR.go #[[]] L).toList =
    #[].toList ++ flatMap ?h.h.false.cons.G (foldr sectionsTR.go #[[]] L).toList

case h.h.false.cons.G
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ List α → List (List α)

case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => acc'.push (a_1 :: a)) acc l).toList = acc.toList ++ ?h.h.false.cons.G a

Proof state:
case h.h
α : Type u_1
L : List (List α)
⊢ L.sections = bif L.any isEmpty then [] else (foldr sectionsTR.go #[[]] L).toList

Tactic:
cases e : L.any isEmpty <;> simp [sections_eq_nil_of_isEmpty, *]

Result:
case h.h.false
α : Type u_1
L : List (List α)
e : L.any isEmpty = false
⊢ L.sections = (foldr sectionsTR.go #[[]] L).toList

Proof state:
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
acc✝ : Array (List α)
a✝ : List α
⊢ (foldl (fun acc' a => acc'.push (a :: a✝)) acc✝ l).toList = acc✝.toList ++ map (fun a => a :: a✝) l

Tactic:
apply Array.foldl_toList_eq_map

Result:
no goals

Proof state:
case h.h.false
α : Type u_1
L : List (List α)
e : L.any isEmpty = false
⊢ L.sections = (foldr sectionsTR.go #[[]] L).toList

Tactic:
clear e

Result:
case h.h.false
α : Type u_1
L : List (List α)
⊢ L.sections = (foldr sectionsTR.go #[[]] L).toList

Proof state:
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
⊢ ∀ (acc : Array (List α)) (a : List α),
    (foldl (fun acc' a_1 => acc'.push (a_1 :: a)) acc l).toList = acc.toList ++ map (fun a_1 => a_1 :: a) l

Tactic:
intros

Result:
case h.h.false.cons.H
α : Type u_1
l : List α
L : List (List α)
IH : L.sections = (foldr sectionsTR.go #[[]] L).toList
acc✝ : Array (List α)
a✝ : List α
⊢ (foldl (fun acc' a => acc'.push (a :: a✝)) acc✝ l).toList = acc✝.toList ++ map (fun a => a :: a✝) l

Proof state:
case h.h
α : Type u_1
L : List (List α)
⊢ L.sections = L.sectionsTR

Tactic:
simp [sectionsTR]

Result:
case h.h
α : Type u_1
L : List (List α)
⊢ L.sections = bif L.any isEmpty then [] else (foldr sectionsTR.go #[[]] L).toList

Proof state:
⊢ @sections = @sectionsTR

Tactic:
funext α L

Result:
case h.h
α : Type u_1
L : List (List α)
⊢ L.sections = L.sectionsTR