awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
rw :
  (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) (sz.splitLengths l) i ⋯).length =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]

Premises used: Nat.lt_add_one, List.getElem_take'
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
simp :
  (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

Tactic:
simp only [take_splitLength]

Premises used: List.take_splitLength
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
rw : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (take (i + 1) sz) i ⋯
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i hi

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]

Premises used: Nat.lt_add_one, List.getElem_take'
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
simp : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (map length ((take (i + 1) sz).splitLengths l)) i ⋯
| getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (take (i + 1) sz) i ⋯

Tactic:
simp +singlePass only [← map_splitLengths_length l _ h]

Premises used: List.map_splitLengths_length
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
rw : (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) (map length ((take (i + 1) sz).splitLengths l)) i ⋯

Tactic:
rw [getElem_map]

Premises used: List.getElem_map
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_1
l : List α
sz : List ℕ
i : ℕ
hi : i < sz.length
h : (take (i + 1) sz).sum ≤ l.length
rw : (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

Tactic:
rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

Premises used: Nat.lt_add_one, List.map_splitLengths_length, List.getElem_map, List.getElem_take'
-- Module: Mathlib.Data.List.SplitLengths
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
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 (List α)) (i : ℕ) ↦ i < as.length) ((take (i + 1) sz).splitLengths l) i ⋯).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

Tactic:
conv_rhs =>
    rw [List.getElem_take' (hj := i.lt_add_one)]
    simp +singlePass only [← map_splitLengths_length l _ h]
    rw [getElem_map]

Premises used: Nat.lt_add_one, List.map_splitLengths_length, List.getElem_map, List.getElem_take'
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α_1 : Type u_1
l_1 : List α_1
sz_1 : List ℕ
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ i < sz.length

Tactic:
simpa using hi
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_2
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ map length (sz.splitLengths l) = sz

Tactic:
have := map_splitLengths_length l sz h
-- Module: Mathlib.Data.List.SplitLengths
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 ⋯
rw₁ : i < (map length (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 ⋯

Tactic:
rw [← List.getElem_map List.length]

Premises used: List.getElem_map, List.length
-- Module: Mathlib.Data.List.SplitLengths
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 ℕ) (i : ℕ) ↦ i < as.length) (map length (sz.splitLengths l)) i ⋯ =
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯

Tactic:
simp [this]
-- Module: Mathlib.Data.List.SplitLengths
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
⊢ i < (map length (sz.splitLengths l)).length

Tactic:
simpa using hi
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
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
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
rw [List.forall_mem_iff_forall_getElem]

Premises used: List.forall_mem_iff_forall_getElem
-- Module: Mathlib.Data.List.SplitLengths
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 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯

Tactic:
have := length_splitLengths_getElem_le l sz (hi := hi)
-- Module: Mathlib.Data.List.SplitLengths
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 ⋯
⊢ i < sz.length

Tactic:
simpa using hi
-- Module: Mathlib.Data.List.SplitLengths
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 ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯ ≤ b

Tactic:
have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)
-- Module: Mathlib.Data.List.SplitLengths
Goal:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this_1 :
  (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 ⋯
this : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) sz i ⋯ ≤ b
⊢ (getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (sz.splitLengths l) i hi).length ≤ b

Tactic:
lia
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List (List α)) (sublists' []) [[]]

Tactic:
rfl

Premises used: List.sublists', rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
⊢ [a].sublists' = [[], [a]]

Tactic:
rfl

Premises used: List.sublists', List.concat, List.get, Array.getInternal, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
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
⊢ sublists'Aux a r₁ r₂ =
    (Array.foldl (fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) r₂.toArray r₁.toArray).toList

Tactic:
rw [sublists'Aux, Array.foldl_toList]

Premises used: List.sublists'Aux, Array.foldl_toList
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    Eq.{u + 1} (α := List (List α)) ((fun (r : List (List α)) (l : List α) ↦ r ++ [a :: l]) x.toList y)
      (Array.toList ((fun (r : Array (List α)) (l : List α) ↦ r.push (a :: l)) x y))

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
⊢ 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)
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r₁ r₂ : List (List α)
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
⊢ 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:
simpa using this
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
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)
⊢ l.sublists' = foldr (fun (a : α) (r : List (List α)) ↦ sublists'Aux a r r) [[]] l

Tactic:
simp only [sublists', sublists'Aux_eq_array_foldl]

Premises used: List.sublists', List.sublists'Aux_eq_array_foldl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
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
⊢ 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:
rw [← List.foldr_hom Array.toList]

Premises used: Array.toList, List.foldr_hom
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
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:
congr
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r₁ x : List (List α)
⊢ sublists'Aux a [] x = x ++ map (cons a) []

Tactic:
simp [sublists'Aux]

Premises used: List.sublists'Aux
-- Module: Mathlib.Data.List.Sublists
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 α)
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]
⊢ sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])

Tactic:
rw [map_append, map_singleton, ← append_assoc, ← ih, sublists'Aux, foldl_append, foldl]

Premises used: List.append_assoc, List.map_singleton, List.sublists'Aux, List.foldl, List.foldl_append, List.map_append
-- Module: Mathlib.Data.List.Sublists
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 α)
⊢ 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:
simp [sublists'Aux]

Premises used: List.sublists'Aux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists' = l.sublists' ++ map (cons a) l.sublists'

Tactic:
simp [sublists'_eq_sublists'Aux, foldr_cons, sublists'Aux_eq_map]

Premises used: List.sublists'Aux_eq_map, List.foldr_cons, List.sublists'_eq_sublists'Aux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
s : List α
nil : s = [] ↔ s <+ []
⊢ Membership.mem (γ := List (List α)) (sublists' []) s ↔ s <+ []

Tactic:
simp only [sublists'_nil, mem_singleton]

Premises used: List.mem_singleton, List.sublists'_nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
s : List α
h : s = []
rw rw₁ : Sublist.{u} (α := α) [] []
⊢ s <+ []

Tactic:
rw [h]
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
s : List α
⊢ s = [] ↔ s <+ []

Tactic:
exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
⊢ s ∈ (a :: t).sublists' ↔ s <+ a :: t

Tactic:
?_
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
s t : List α
cons :
  ∀ (a : α) (t : List α) (IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t) {s : List α},
    s ∈ (a :: t).sublists' ↔ s <+ a :: t
⊢ s ∈ t.sublists' ↔ s <+ 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 => ?_

Premises used: List.mem_singleton, List.cons, List.sublists'_nil, List.nil
-- Module: Mathlib.Data.List.Sublists
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 ∈ (a :: t).sublists' ↔ s <+ a :: t

Tactic:
simp only [sublists'_cons, mem_append, IH, mem_map]

Premises used: List.sublists'_cons, List.mem_append, List.mem_map
-- Module: Mathlib.Data.List.Sublists
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
cons₁ : s <+ a :: t → s <+ t ∨ ∃ (a_2 : List α), a_2 <+ t ∧ a :: a_2 = s
⊢ (s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s) ↔ s <+ a :: t

Tactic:
constructor
-- Module: Mathlib.Data.List.Sublists
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
cons₁ : ∀ (s : List α) (h : s <+ t), a :: s <+ a :: t
⊢ s <+ a :: t

Tactic:
rcases h with (h | ⟨s, h, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

Tactic:
sublist_cons_of_sublist _ h

Premises used: List.sublist_cons_of_sublist
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ a :: t

Tactic:
exact sublist_cons_of_sublist _ h

Premises used: List.sublist_cons_of_sublist
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
h.cons_cons _

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ a :: s <+ a :: t

Tactic:
exact h.cons_cons _

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sublists
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
cons₁ : ∀ {l₁ : List α} (h : l₁ <+ t), a :: l₁ <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = a :: l₁
⊢ s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s

Tactic:
obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t
⊢ s <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = s

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁ : List α
h : l₁ <+ t
⊢ a :: l₁ <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = a :: l₁

Tactic:
Or.inr ⟨_, h, rfl⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
l₁ : List α
h : l₁ <+ t
⊢ a :: l₁ <+ t ∨ ∃ (a_1 : List α), a_1 <+ t ∧ a :: a_1 = a :: l₁

Tactic:
exact Or.inr ⟨_, h, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists'.length = HPow.hPow (α := ℕ) 2 (a :: l).length

Tactic:
simp +arith only [sublists'_cons, length_append, length_sublists' l,
      length_map, length, Nat.pow_succ']

Premises used: Nat.pow_succ', List.length_append, List.sublists'_cons, List.length_map, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List (List α)) (sublists []) [[]]

Tactic:
rfl

Premises used: List.sublists, List.foldr, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
⊢ [a].sublists = [[], [a]]

Tactic:
rfl

Premises used: List.sublists, List.append, List.foldr, rfl, List.flatten
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
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)
⊢ 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)

Tactic:
funext a r
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r : List (List α)
⊢ ∀ (x : Array (List α)) (y : List α),
    Eq.{u + 1} (α := List (List α)) ((fun (r : List (List α)) (l : List α) ↦ r ++ [l, a :: l]) x.toList y)
      (Array.toList ((fun (r : Array (List α)) (l : List α) ↦ (r.push l).push (a :: l)) x y))

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r : List (List α)
⊢ 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)
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r : List (List α)
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))
⊢ 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))

Tactic:
simpa using this
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r : List (List α)
⊢ sublistsAux a [] = flatMap (fun (l : List α) ↦ [l, a :: l]) []

Tactic:
simp [sublistsAux]

Premises used: List.sublistsAux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r_1 r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun (l : List α) ↦ [l, a :: l]) r
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]
⊢ sublistsAux a (r ++ [l]) = flatMap (fun (l : List α) ↦ [l, a :: l]) (r ++ [l])

Tactic:
rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]

Premises used: List.foldl_append, List.flatMap_singleton, List.flatMap_append, List.sublistsAux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
r_1 r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun (l : List α) ↦ [l, a :: l]) r
⊢ 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:
simp [sublistsAux]

Premises used: List.sublistsAux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
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₁)
⊢ (l₁ ++ l₂).sublists = do
    let x ← l₂.sublists
    map (fun (x_1 : List α) ↦ x_1 ++ x) l₁.sublists

Tactic:
simp only [sublists, foldr_append]

Premises used: List.sublists, List.foldr_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
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₂) [])
    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:
simp