awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
have nil : ∀ (l : List α) {i : ℕ} {hi : i < (splitLengths [] l).length},
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (splitLengths [] l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] i sorry
Tactic: induction sz generalizing l i
Cleared hypotheses: l, sz, i, hi
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < (sz.splitLengths l).length
nil :
  ∀ (l : List α) {i : ℕ} {hi : i < (splitLengths [] l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (splitLengths [] l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] i ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
      (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i sorry) →
    ∀ (l : List α) {i : ℕ} {hi : i < ((head :: tail).splitLengths l).length},
      (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((head :: tail).splitLengths l) i
            hi).length ≤
        getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i sorry
Tactic: induction sz generalizing l i
Cleared hypotheses: l, sz, i, hi
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((head :: tail).splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯
have simp : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l)) i
      sorry).length ≤
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i sorry
Tactic: simp only [splitLengths_cons]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        i ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯
have zero : ∀ {hi : 0 < ((head :: tail).splitLengths l).length},
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        0 sorry).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 sorry
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
tail_ih :
  ∀ (l : List α) {i : ℕ} {hi : i < (tail.splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tail.splitLengths l) i hi).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail i ⋯
l : List α
i : ℕ
hi : i < ((head :: tail).splitLengths l).length
zero :
  ∀ {hi : 0 < ((head :: tail).splitLengths l).length},
    (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length)
          (take head l :: tail.splitLengths (drop head l)) 0 ⋯).length ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        i ⋯).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) i ⋯
have succ : ∀ (n : ℕ) {hi : n + 1 < ((head :: tail).splitLengths l).length},
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take head l :: tail.splitLengths (drop head l))
        (n + 1) sorry).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1) sorry
Tactic: cases i
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : l.length ≤ sz.sum
⊢ (sz.splitLengths l).flatten = l
have nil : ∀ (l : List α) (h : l.length ≤ sum []), (splitLengths [] l).flatten = l
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz, h
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : l.length ≤ sz.sum
nil : ∀ (l : List α) (h : l.length ≤ sum []), (splitLengths [] l).flatten = l
⊢ (sz.splitLengths l).flatten = l
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l) →
    ∀ (l : List α) (h : l.length ≤ (head :: tail).sum), ((head :: tail).splitLengths l).flatten = l
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz, h
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ ((head :: tail).splitLengths l).flatten = l
have simp : take head l ++ (tail.splitLengths (drop head l)).flatten = l
Tactic: simp only [splitLengths_cons, flatten_cons]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : l.length ≤ tail.sum), (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ take head l ++ (tail.splitLengths (drop head l)).flatten = l
have h₁ : (drop head l).length ≤ tail.sum
Tactic: rw [ih, take_append_drop]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
⊢ map length (sz.splitLengths l) = sz
have nil : ∀ (l : List α) (h : sum [] ≤ l.length), map length (splitLengths [] l) = []
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz, h
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
nil : ∀ (l : List α) (h : sum [] ≤ l.length), map length (splitLengths [] l) = []
⊢ map length (sz.splitLengths l) = sz
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail) →
    ∀ (l : List α) (h : (head :: tail).sum ≤ l.length), map length ((head :: tail).splitLengths l) = head :: tail
Tactic: induction sz generalizing l
Cleared hypotheses: l, sz, h
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail
have simp : head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail
Tactic: simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail
have rw : head ≤ l.length ∧ tail = tail
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α) (h : tail.sum ≤ l.length), map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
rw : head ≤ l.length ∧ tail = tail
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail
have h₁ : tail.sum ≤ (drop head l).length
Tactic: rw [ih]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have rw : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (i + 1) (sz.splitLengths l)) i sorry).length =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
Tactic: rw [List.getElem_take' (hj := i.lt_add_one)]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (i + 1) (sz.splitLengths l)) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have simp : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
Tactic: simp only [take_splitLength]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have rw : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (take (i + 1) sz) i sorry
Tactic: rw [List.getElem_take' (hj := i.lt_add_one)]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (take (i + 1) sz) i ⋯
have simp : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (map length ((take (i + 1) sz).splitLengths l)) i sorry
Tactic: simp +singlePass only [← map_splitLengths_length l _ h]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (map length ((take (i + 1) sz).splitLengths l)) i ⋯
have rw : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length
Tactic: rw [getElem_map]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have rw : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length
Tactic: rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have conv_rhs : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
Tactic: conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
conv_rhs :
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi
have conv_rhs₁ : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length =
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i sorry).length
Tactic: conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (hypothesis)
Goal:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
have this : map length (sz.splitLengths l) = sz
Tactic: have := map_splitLengths_length l sz h
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
have rw : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (map length (sz.splitLengths l)) i sorry =
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i sorry
Tactic: rw [← List.getElem_map List.length]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
this : map length (sz.splitLengths l) = sz
rw :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (map length (sz.splitLengths l)) i ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
have rw₁ : i < (map length (sz.splitLengths l)).length
Tactic: rw [← List.getElem_map List.length]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (goal)
Goal:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b
have rw : ∀ (i : ℕ) (hi : i < (sz.splitLengths l).length),
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤ b
Tactic: rw [List.forall_mem_iff_forall_getElem]
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (hypothesis)
Goal:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤ b
have this : (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i sorry
Tactic: have := length_splitLengths_getElem_le l sz (hi := hi)
-- Lean 4 proof step from Mathlib.Data.List.SplitLengths (hypothesis)
Goal:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this :
  (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤ b
have this₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i sorry ≤ b
Tactic: have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ sublists'Aux a r₁ r₂ =
    (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
have rw : Array.foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l]) r₂ { toList := r₁ : Array (List α) } =
  (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
Tactic: rw [sublists'Aux, Array.foldl_toList]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ Array.foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l]) r₂ { toList := r₁ : Array (List α) } =
    (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList
have this : foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l]) r₂.toArray.toList r₁ =
  (foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r₂.toArray r₁).toList
Tactic: have := List.foldl_hom Array.toList (g₁ := fun r l => r.push (a :: l))
    (g₂ := fun r l => r ++ [a :: l]) (l := r₁) (init := r₂.toArray) (by simp)
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.sublists' = foldr (fun (a : α) (r : List (List α)) ↦ sublists'Aux a r r) [[]] l
have simp : Eq (α := List (List α))
  (Array.toList
    (foldr
      (fun (a : α) (arr : Array (List α)) ↦
        Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) arr arr)
      #[[]] l))
  (foldr
    (fun (a : α) (r : List (List α)) ↦
      (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r.toArray r.toArray).toList)
    [[]] l)
Tactic: simp only [sublists', sublists'Aux_eq_array_foldl]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ Eq (α := List (List α))
    (Array.toList
      (foldr
        (fun (a : α) (arr : Array (List α)) ↦
          Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) arr arr)
        #[[]] l))
    (foldr
      (fun (a : α) (r : List (List α)) ↦
        (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r.toArray r.toArray).toList)
      [[]] l)
have rw : ∀ (x : α) (y : Array (List α)),
  (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (x :: l)) y.toList.toArray y.toList.toArray).toList =
    (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (x :: l)) y y).toList
Tactic: rw [← List.foldr_hom Array.toList]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
r₁_1 r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])
have rw : foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l])
    (foldl (fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
  sublists'Aux a r₁ r₂ ++ [a :: l]
Tactic: rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s : List α
⊢ Membership.mem (γ := List (List α)) (sublists' []) s ↔ s <+ []
have nil : s = [] ↔ s <+ []
Tactic: simp only [sublists'_nil, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s : List α
h : s = []
⊢ s <+ []
have rw : Sublist.{u} (α := α) [] []
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t
have cons : ∀ (a : α) (t : List α) (IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t) {s : List α},
  s ∈ (a :: t).sublists' ↔ s <+ a :: t
Tactic: induction t generalizing s with
  | nil =>
    simp only [sublists'_nil, mem_singleton]
    exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
  | cons a t IH => ?_
Cleared hypotheses: s, t
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t
have cons : (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
Tactic: simp only [sublists'_cons, mem_append, IH, mem_map]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
have cons : (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
cons : (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) → s <+ a :: t
⊢ (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t
have cons₁ : s <+ a :: t → s <+ t ∨ ∃ (a_2 : List α), a_2 <+ t ∧ a :: a_2 = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t
have cons : ∀ (h : s <+ t), s <+ a :: t
Tactic: rcases h with (h | ⟨s, h, rfl⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
cons : ∀ (h : s <+ t), s <+ a :: t
⊢ s <+ a :: t
have cons₁ : ∀ (s : List α) (h : s <+ t), a :: s <+ a :: t
Tactic: rcases h with (h | ⟨s, h, rfl⟩)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
⊢ s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
have cons : ∀ (h : s <+ t), s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
Tactic: obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ a :: t
cons : ∀ (h : s <+ t), s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s
have cons₁ : ∀ {l₁ : List α} (h : l₁ <+ t), a :: l₁ <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = a :: l₁
Tactic: obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := (a : α) → (r : List (List α)) → List (List α)) sublistsAux fun (a : α) (r : List (List α)) ↦
    Array.toList (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ (r.push l).push (a :: l)) #[] r.toArray)
have h : ∀ (a : α) (r : List (List α)),
  sublistsAux a r =
    Array.toList (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ (r.push l).push (a :: l)) #[] r.toArray)
Tactic: funext a r