α : 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₁)
simp only [sublists_eq_sublistsAux, foldr_append, sublistsAux_eq_bind]
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]) [[]] [])

case cons
α : 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✝)
⊢ 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₂)
      (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 α
⊢ 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₁)
induction l₁
case cons
α : 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✝)
⊢ 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₂)
      (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]) [[]] [])

case cons
α : 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✝)
⊢ 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₂)
      (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 => simp
no goals
case cons
α : 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✝)
⊢ 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₂)
      (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 l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.bind, join_join, Function.comp]
no goals
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]) [[]] [])
case nil => simp
no goals
α : 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
no goals
case cons
α : 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✝)
⊢ 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₂)
      (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 l₁ ih =>
  rw [foldr_cons, ih]
  simp [List.bind, join_join, Function.comp]
α : 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₁))
rw [foldr_cons, ih]
no goals
α : 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₁))
simp [List.bind, join_join, Function.comp]