awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
a : α
r : List (List α)
⊢ Eq (α := List (List α)) (foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [l, a :: l]) [] r)
    (Array.toList (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ (r.push l).push (a :: l)) #[] r.toArray))
have this : Eq (α := List (List α)) (foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [l, a :: l]) (Array.toList #[]) r)
  (Array.toList (foldl (fun (r : Array (List α)) (l : List α) ↦ (r.push l).push (a :: l)) #[] r))
Tactic: have := foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l))
    (g₂ := fun r l => r ++ [l, a :: l]) (l := r) (init := #[]) (by simp)
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
r_1 r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun (l : List α) ↦ [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun (l : List α) ↦ [l, a :: l]) (r ++ [l])
have rw : foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [l, a :: l])
    (foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [l, a :: l]) [] r) [l] =
  sublistsAux a r ++ [l, a :: l]
Tactic: rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    map (fun (x_1 : List α) ↦ x_1 ++ x) l₁.sublists
have simp : Eq (α := List (List α))
  (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) l₁)
  do
  let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
  map (fun (x_1 : List α) ↦ x_1 ++ x)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁)
Tactic: simp only [sublists, foldr_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) l₁)
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁)
⊢ Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) (a :: l₁))
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] (a :: l₁))
have cons : Eq (α := List (List α))
  (flatMap (fun (x : List α) ↦ [x, a :: x]) do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁))
  do
  let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
  map (fun (x_1 : List α) ↦ x_1 ++ x)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] (a :: l₁))
Tactic: rw [foldr_cons, ih]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ : List α
⊢ Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) l₁)
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁)
have nil : Eq (α := List (List α))
  (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) [])
  do
  let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
  map (fun (x_1 : List α) ↦ x_1 ++ x)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] [])
Tactic: induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ : List α
nil :
  Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) [])
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] [])
⊢ Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) l₁)
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁)
have cons : ∀ (a : α) (l₁ : List α)
  (ih :
    Eq (α := List (List α))
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) l₁)
      do
      let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
      map (fun (x_1 : List α) ↦ x_1 ++ x)
          (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₁)),
  Eq (α := List (List α))
    (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc)
      (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂) (a :: l₁))
    do
    let x ← foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] l₂
    map (fun (x_1 : List α) ↦ x_1 ++ x)
        (foldr (fun (a : α) (acc : List (List α)) ↦ flatMap (fun (x : List α) ↦ [x, a :: x]) acc) [[]] (a :: l₁))
Tactic: induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
l : List α
⊢ ([a] ++ l).sublists = do
    let x ← l.sublists
    [x, a :: x]
have rw : Eq (α := List (List α))
  (do
    let x ← l.sublists
    map (fun (x_1 : List α) ↦ x_1 ++ x) [a].sublists)
  do
  let x ← l.sublists
  [x, a :: x]
Tactic: rw [sublists_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw : (do
    let x ← [a].sublists
    map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₁ : (do
    let x ← [[], [a]]
    map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₂ : flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₂ :
  flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₃ : HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ []) l.sublists)
    (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[a]]) =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₂ :
  flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₃ :
  HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ []) l.sublists)
      (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[a]]) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₄ : map (fun (x : List α) ↦ x ++ []) l.sublists ++
    HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists)
      (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) []) =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₂ :
  flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₃ :
  HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ []) l.sublists)
      (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[a]]) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₄ :
  map (fun (x : List α) ↦ x ++ []) l.sublists ++
      HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists)
        (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) []) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₅ : map (fun (x : List α) ↦ x ++ []) l.sublists ++
    HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists) [] =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₂ :
  flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₃ :
  HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ []) l.sublists)
      (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[a]]) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₄ :
  map (fun (x : List α) ↦ x ++ []) l.sublists ++
      HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists)
        (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) []) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₅ :
  map (fun (x : List α) ↦ x ++ []) l.sublists ++
      HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists) [] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₆ : l.sublists ++ HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists) [] =
  l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
rw :
  (do
      let x ← [a].sublists
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₁ :
  (do
      let x ← [[], [a]]
      map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₂ :
  flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[], [a]] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₃ :
  HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ []) l.sublists)
      (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) [[a]]) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₄ :
  map (fun (x : List α) ↦ x ++ []) l.sublists ++
      HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists)
        (flatMap (fun (x : List α) ↦ map (fun (x_1 : List α) ↦ x_1 ++ x) l.sublists) []) =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₅ :
  map (fun (x : List α) ↦ x ++ []) l.sublists ++
      HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists) [] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
rw₆ :
  l.sublists ++ HAppend.hAppend (α := List (List α)) (map (fun (x : List α) ↦ x ++ [a]) l.sublists) [] =
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
have rw₇ : l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists = l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.reverse.sublists = map reverse l.sublists'
have nil : Eq.{u + 1} (α := List (List α)) (sublists (reverse [])) (map reverse (sublists' []))
Tactic: induction l with
  | nil => rfl
  | cons hd tl ih =>
    simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
      bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil, Function.comp_def]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List (List α)) (sublists (reverse [])) (map reverse (sublists' []))
⊢ l.reverse.sublists = map reverse l.sublists'
have cons : ∀ (hd : α) (tl : List α) (ih : tl.reverse.sublists = map reverse tl.sublists'),
  (hd :: tl).reverse.sublists = map reverse (hd :: tl).sublists'
Tactic: induction l with
  | nil => rfl
  | cons hd tl ih =>
    simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
      bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil, Function.comp_def]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.sublists = map reverse l.reverse.sublists'
have rw : l.sublists = l.reverse.reverse.sublists
Tactic: rw [← sublists_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
rw : l.sublists = l.reverse.reverse.sublists
⊢ l.sublists = map reverse l.reverse.sublists'
have rw₁ : l.sublists = l.sublists
Tactic: rw [← sublists_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.sublists' = map reverse l.reverse.sublists
have rw : l.sublists' = l.reverse.reverse.sublists'
Tactic: rw [← sublists'_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
rw : l.sublists' = l.reverse.reverse.sublists'
⊢ l.sublists' = map reverse l.reverse.sublists
have rw₁ : l.sublists' = l.sublists'
Tactic: rw [← sublists'_reverse, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s <+ t
have rw : s ∈ t.sublists ↔ s.reverse <+ t.reverse
Tactic: rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s t : List α
rw : s ∈ t.sublists ↔ s.reverse <+ t.reverse
⊢ s ∈ t.sublists ↔ s <+ t
have rw₁ : s ∈ t.sublists ↔ s.reverse ∈ t.reverse.sublists'
Tactic: rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s t : List α
rw : s ∈ t.sublists ↔ s.reverse <+ t.reverse
rw₁ : s ∈ t.sublists ↔ s.reverse ∈ t.reverse.sublists'
⊢ s ∈ t.sublists ↔ s <+ t
have rw₂ : s ∈ t.sublists ↔ s.reverse ∈ map reverse t.sublists
Tactic: rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s t : List α
rw : s ∈ t.sublists ↔ s.reverse <+ t.reverse
rw₁ : s ∈ t.sublists ↔ s.reverse ∈ t.reverse.sublists'
rw₂ : s ∈ t.sublists ↔ s.reverse ∈ map reverse t.sublists
⊢ s ∈ t.sublists ↔ s <+ t
have rw₃ : s ∈ t.sublists ↔ s ∈ t.sublists
Tactic: rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ map pure l <+ l.sublists
have nil : Sublist.{u} (α := List α) (map pure []) (sublists [])
Tactic: induction l using reverseRecOn
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
nil : Sublist.{u} (α := List α) (map pure []) (sublists [])
⊢ map pure l <+ l.sublists
have append_singleton : ∀ (l : List α) (a : α), map pure l <+ l.sublists → map pure (l ++ [a]) <+ (l ++ [a]).sublists
Tactic: induction l using reverseRecOn
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
h : map pure l <+ l.sublists
⊢ map pure (l ++ [a]) <+ (l ++ [a]).sublists
have append_singleton : HAppend.hAppend (α := List (List α)) (map pure l) [pure a] <+ l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
Tactic: simp only [map, map_append, sublists_concat]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s
have unfold : (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
Tactic: unfold sublistsLenAux
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s
have unfold : sublistsLenAux (n + 1) l (g ∘ f) (sublistsLenAux n l ((g ∘ f) ∘ cons a) (map g r ++ s)) =
  map g (sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ cons a) r)) ++ s
Tactic: unfold sublistsLenAux
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r
have rw : sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
Tactic: rw [sublistsLen, ← sublistsLenAux_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
l : List α
f : List α → β
r : List β
⊢ sublistsLenAux 0 l f r = f [] :: r
have nil : sublistsLenAux 0 [] f r = f [] :: r
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
l : List α
f : List α → β
r : List β
nil : sublistsLenAux 0 [] f r = f [] :: r
⊢ sublistsLenAux 0 l f r = f [] :: r
have cons : ∀ (head : α) (tail : List α), sublistsLenAux 0 (head :: tail) f r = f [] :: r
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
have rw : sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
Tactic: rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
      append_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ Eq.{u + 1} (α := List (List α)) (sublistsLen 1 []) (map (fun (x : α) ↦ [x]) (reverse []))
have rw : Eq.{u + 1} (α := List (List α)) [] (map (fun (x : α) ↦ [x]) (reverse []))
Tactic: rw [sublistsLen_succ_nil, reverse_nil, map_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
rw : Eq.{u + 1} (α := List (List α)) [] (map (fun (x : α) ↦ [x]) (reverse []))
⊢ Eq.{u + 1} (α := List (List α)) (sublistsLen 1 []) (map (fun (x : α) ↦ [x]) (reverse []))
have rw₁ : Eq.{u + 1} (α := List (List α)) [] (map (fun (x : α) ↦ [x]) [])
Tactic: rw [sublistsLen_succ_nil, reverse_nil, map_nil]