-- Mathlib/Data/List/Sublists.lean
theorem range_bind_sublistsLen_perm (l : List α) :
    ((List.range (l.length + 1)).flatMap fun n => sublistsLen n l) ~ sublists' l

Proof state:
case nil
α : Type u
⊢ flatMap (fun n => sublistsLen n []) (range ([].length + 1)) ~ [].sublists'

Tactic:
simp [range_succ]

Result:
no goals

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
exact l_ih

Result:
no goals

Proof state:
α : Type u
l : List α
⊢ flatMap (fun n => sublistsLen n l) (range (l.length + 1)) ~ l.sublists'

Tactic:
induction' l with h tl l_ih

Result:
case nil
α : Type u
⊢ flatMap (fun n => sublistsLen n []) (range ([].length + 1)) ~ [].sublists'

case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n => sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a => sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
refine Perm.append ?_ (l_ih.map _)

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a => sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
rw [← List.singleton_append, ← List.sublistsLen_zero tl]

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a => sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a => map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
simp_rw [← List.map_flatMap, ← cons_append]

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a => sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a => sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a => map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n => sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Tactic:
simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
  sublists'_cons, List.sublistsLen_zero, List.singleton_append]

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a => sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Proof state:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a => sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
rw [List.range_succ, flatMap_append, flatMap_singleton,
  sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
  ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
  ← flatMap_cons 0 _ fun n => sublistsLen n tl, ← range_succ_eq_map]

Result:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n => sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'