-- Mathlib/Data/List/Sublists.lean
theorem sublists_append (l₁ l₂ : List α) :
    sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x))

Proof state:
case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)
⊢ (flatMap (fun x => [x, a :: x]) do
      let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
      map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)) =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
simp [List.flatMap, flatten_flatten, Function.comp_def]

Result:
no goals

Proof state:
case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)
⊢ foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) (a :: l₁) =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
rw [foldr_cons, ih]

Result:
case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)
⊢ (flatMap (fun x => [x, a :: x]) do
      let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
      map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)) =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] (a :: l₁))

Proof state:
α : Type u
l₁ l₂ : List α
⊢ foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)

Tactic:
induction l₁ with
| nil => simp
| cons a l₁ ih =>
  rw [foldr_cons, ih]
  simp [List.flatMap, flatten_flatten, Function.comp_def]

Result:
no goals

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

Tactic:
simp only [sublists, foldr_append]

Result:
α : Type u
l₁ l₂ : List α
⊢ foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) l₁ =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₁)

Proof state:
case nil
α : Type u
l₂ : List α
⊢ foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc)
      (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂) [] =
    do
    let x ← foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] l₂
    map (fun x_1 => x_1 ++ x) (foldr (fun a acc => flatMap (fun x => [x, a :: x]) acc) [[]] [])

Tactic:
simp

Result:
no goals