case nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ (List.bind (range (length [] + 1)) fun n => sublistsLen n []) ~ sublists' []

case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length (h :: tl) + 1)) fun n => sublistsLen n (h :: tl)) ~ sublists' (h :: tl)
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
l : List α
⊢ (List.bind (range (length l + 1)) fun n => sublistsLen n l) ~ sublists' l
induction' l with h tl l_ih
no goals
case nil
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
⊢ (List.bind (range (length [] + 1)) fun n => sublistsLen n []) ~ sublists' []
simp [range_succ]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length (h :: tl) + 1)) fun n => sublistsLen n (h :: tl)) ~ sublists' (h :: tl)
simp_rw [range_succ_eq_map, length, cons_bind, map_bind, sublistsLen_succ_cons, sublists'_cons,
  List.sublistsLen_zero, List.singleton_append]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ [] ::
      ((List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
        List.bind (range (length tl + 1)) fun a => map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
refine' ((bind_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans _
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ [] ::
      ((List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
        List.bind (range (length tl + 1)) fun a => map (cons h) (sublistsLen a tl)) ~
    sublists' tl ++ map (cons h) (sublists' tl)
simp_rw [← List.bind_map, ← cons_append]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ ([] :: List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
rw [← List.singleton_append, ← List.sublistsLen_zero tl]
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ~ sublists' tl
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ++
      map (cons h) (List.bind (range (length tl + 1)) fun a => sublistsLen a tl) ~
    sublists' tl ++ map (cons h) (sublists' tl)
refine' Perm.append _ (l_ih.map _)
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (sublistsLen 0 tl ++ List.bind (range (length tl + 1)) fun a => sublistsLen (a + 1) tl) ~ sublists' tl
rw [List.range_succ, append_bind, bind_singleton,
  sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil, ←
  List.map_bind (fun n => sublistsLen n tl) Nat.succ, ←
  cons_bind 0 _ fun n => sublistsLen n tl, ← range_succ_eq_map]
no goals
case cons
α✝ : Type u
β : Type v
γ : Type w
α : Type u_1
h : α
tl : List α
l_ih : (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
⊢ (List.bind (range (length tl + 1)) fun n => sublistsLen n tl) ~ sublists' tl
exact l_ih