awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sublists
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₁)
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₁))
⊢ 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:
rw [foldr_cons, ih]

Premises used: List.foldr_cons
-- Module: Mathlib.Data.List.Sublists
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 α))
    (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:
simp [List.flatMap, flatten_flatten, Function.comp_def]

Premises used: List.flatten_flatten, Function.comp_def, List.flatMap
-- Module: Mathlib.Data.List.Sublists
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) [[]] [])
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₁))
⊢ 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:
induction l₁ with
  | nil => simp
  | cons a l₁ ih =>
    rw [foldr_cons, ih]
    simp [List.flatMap, flatten_flatten, Function.comp_def]

Premises used: List.foldr_cons, List.flatten_flatten, List.cons, Function.comp_def, List.flatMap, List.nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
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]
⊢ ([a] ++ l).sublists = do
    let x ← l.sublists
    [x, a :: x]

Tactic:
rw [sublists_append]

Premises used: List.sublists_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
⊢ 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:
simp only [sublists_singleton, map_cons, bind_eq_flatMap, nil_append, cons_append, map_nil]

Premises used: List.map_cons, List.sublists_singleton, List.bind_eq_flatMap, List.nil_append, List.cons_append, List.map_nil
-- Module: Mathlib.Data.List.Sublists
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
rw₇ rw₈ :
  l.sublists ++ 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

Tactic:
rw [sublists_append, sublists_singleton, bind_eq_flatMap, flatMap_cons, flatMap_cons, flatMap_nil,
     map_id'' append_nil, append_nil]

Premises used: List.sublists_singleton, List.flatMap_nil, List.sublists_append, List.append_nil, List.flatMap_cons, List.bind_eq_flatMap, List.map_id''
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
⊢ Eq.{u + 1} (α := List (List α)) (sublists (reverse [])) (map reverse (sublists' []))

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
hd : α
tl : List α
ih : tl.reverse.sublists = map reverse tl.sublists'
⊢ (hd :: tl).reverse.sublists = map reverse (hd :: tl).sublists'

Tactic:
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]

Premises used: List.sublists_singleton, List.flatMap_nil, List.map_map, List.sublists'_cons, List.sublists_append, List.append_nil, List.flatMap_cons, List.bind_eq_flatMap, List.reverse_cons, Function.comp_def, List.map_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
nil : Eq.{u + 1} (α := List (List α)) (sublists (reverse [])) (map reverse (sublists' []))
cons :
  ∀ (hd : α) (tl : List α) (ih : tl.reverse.sublists = map reverse tl.sublists'),
    (hd :: tl).reverse.sublists = map reverse (hd :: tl).sublists'
⊢ l.reverse.sublists = map reverse l.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]

Premises used: List.sublists_singleton, List.flatMap_nil, List.map_map, List.sublists'_cons, List.sublists_append, List.append_nil, List.cons, List.flatMap_cons, List.bind_eq_flatMap, List.reverse_cons, Function.comp_def, List.map_append, List.nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
rw : l.sublists = l.reverse.reverse.sublists
rw₁ rw₂ : l.sublists = l.sublists
⊢ l.sublists = map reverse l.reverse.sublists'

Tactic:
rw [← sublists_reverse, reverse_reverse]

Premises used: List.sublists_reverse, List.reverse_reverse
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ l.reverse.sublists' = map reverse l.sublists

Tactic:
simp only [sublists_eq_sublists', map_map, map_id'' reverse_reverse, Function.comp_def]

Premises used: List.map_map, List.sublists_eq_sublists', Function.comp_def, List.reverse_reverse, List.map_id''
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
rw : l.sublists' = l.reverse.reverse.sublists'
rw₁ rw₂ : l.sublists' = l.sublists'
⊢ l.sublists' = map reverse l.reverse.sublists

Tactic:
rw [← sublists'_reverse, reverse_reverse]

Premises used: List.reverse_reverse, List.sublists'_reverse
-- Module: Mathlib.Data.List.Sublists
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
rw₃ rw₄ : s ∈ t.sublists ↔ s ∈ t.sublists
⊢ s ∈ t.sublists ↔ s <+ t

Tactic:
rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
    mem_map_of_injective reverse_injective]

Premises used: List.reverse_injective, List.reverse_sublist, List.mem_sublists', List.mem_map_of_injective, List.sublists'_reverse
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ l.sublists.length = HPow.hPow (α := ℕ) 2 l.length

Tactic:
simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]

Premises used: List.length_reverse, List.sublists_eq_sublists', List.length_map, List.length_sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
nil : Sublist.{u} (α := List α) (map pure []) (sublists [])
append_singleton : ∀ (l : List α) (a : α), map pure l <+ l.sublists → map pure (l ++ [a]) <+ (l ++ [a]).sublists
⊢ map pure l <+ l.sublists

Tactic:
induction l using reverseRecOn
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
a : α
h : map pure l <+ l.sublists
append_singleton :
  HAppend.hAppend (α := List (List α)) (map pure l) [pure a] <+
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists
⊢ map pure (l ++ [a]) <+ (l ++ [a]).sublists

Tactic:
simp only [map, map_append, sublists_concat]

Premises used: List.map, List.sublists_concat, List.map_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
⊢ Sublist.{u} (α := List α) [] (sublists [])

Tactic:
simp only [sublists_nil, sublist_cons_self]

Premises used: List.sublist_cons_self, List.sublists_nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ [] ++ [a] = pure a

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
a : α
ih : map pure l <+ l.sublists
⊢ HAppend.hAppend (α := List (List α)) (map pure l) [pure a] <+
    l.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l.sublists

Tactic:
exact ((append_sublist_append_left _).2 <|
              singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
          ((append_sublist_append_right _).2 ih)

Premises used: List.append_sublist_append_left, Iff.mpr, List.append_sublist_append_right, And.intro, List.Sublist.trans, Exists.intro, List.nil_sublist, List.mem_sublists, List.mem_map, List.singleton_sublist, List.nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
unfold : (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s
⊢ sublistsLenAux 0 l (g ∘ f) (map g r ++ s) = map g (sublistsLenAux 0 l f r) ++ s

Tactic:
unfold sublistsLenAux

Premises used: List.sublistsLenAux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
γ : Type w
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) [] :: (map g r ++ s) = map g (f [] :: r) ++ s

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
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
⊢ sublistsLenAux (n + 1) (a :: l) (g ∘ f) (map g r ++ s) = map g (sublistsLenAux (n + 1) (a :: l) f r) ++ s

Tactic:
unfold sublistsLenAux

Premises used: List.sublistsLenAux
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ (g ∘ f) ∘ cons a = g ∘ f ∘ cons a

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
γ : Type w
n : ℕ
a : α
l : List α
f : List α → β
g : β → γ
r : List β
s : List γ
⊢ 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:
simp only [show (g ∘ f) ∘ List.cons a = g ∘ f ∘ List.cons a by rfl,
      sublistsLenAux_append]
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
rw : sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
⊢ sublistsLenAux n l f r = map f (sublistsLen n l) ++ r

Tactic:
rw [sublistsLen, ← sublistsLenAux_append]

Premises used: List.sublistsLen, List.sublistsLenAux_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
l : List α
f : List α → β
r : List β
nil : sublistsLenAux 0 [] f r = f [] :: r
cons : ∀ (head : α) (tail : List α), sublistsLenAux 0 (head :: tail) f r = f [] :: r
⊢ sublistsLenAux 0 l f r = f [] :: r

Tactic:
cases l
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : List α → β
r : List β
⊢ sublistsLenAux 0 [] f r = f [] :: r

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : List α → β
r : List β
head : α
tail : List α
⊢ sublistsLenAux 0 (head :: tail) f r = f [] :: r

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ sublistsLen 0 l = [[]]

Tactic:
sublistsLenAux_zero _ _ _

Premises used: List.sublistsLenAux_zero, List.sublistsLen
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
⊢ Eq.{u + 1} (α := List (List α)) (sublistsLen (n + 1) []) []

Tactic:
rfl

Premises used: List.sublistsLenAux, List.sublistsLen, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
rw :
  sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
⊢ sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
rw [sublistsLen, sublistsLenAux, sublistsLenAux_eq, sublistsLenAux_eq, map_id,
      append_nil]

Premises used: List.sublistsLenAux_eq, List.sublistsLenAux, List.map_id, List.sublistsLen, List.append_nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
rw : Eq.{u + 1} (α := List (List α)) [] (map (fun (x : α) ↦ [x]) (reverse []))
rw₁ : Eq.{u + 1} (α := List (List α)) [] (map (fun (x : α) ↦ [x]) [])
rw₂ rw₃ : Eq.{u + 1} (α := List (List α)) [] []
⊢ Eq.{u + 1} (α := List (List α)) (sublistsLen 1 []) (map (fun (x : α) ↦ [x]) (reverse []))

Tactic:
rw [sublistsLen_succ_nil, reverse_nil, map_nil]

Premises used: List.sublistsLen_succ_nil, List.reverse_nil, List.map_nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun (x : α) ↦ [x]) s.reverse
rw :
  map (fun (x : α) ↦ [x]) s.reverse ++ map (cons a) [[]] =
    HAppend.hAppend (α := List (List α)) (map (fun (x : α) ↦ [x]) s.reverse) (map (fun (x : α) ↦ [x]) [a])
⊢ sublistsLen 1 (a :: s) = map (fun (x : α) ↦ [x]) (a :: s).reverse

Tactic:
rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]

Premises used: List.sublistsLen_succ_cons, List.reverse_cons, List.map_append, List.sublistsLen_zero
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun (x : α) ↦ [x]) s.reverse
⊢ map (fun (x : α) ↦ [x]) s.reverse ++ map (cons a) [[]] =
    HAppend.hAppend (α := List (List α)) (map (fun (x : α) ↦ [x]) s.reverse) (map (fun (x : α) ↦ [x]) [a])

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ (sublistsLen 0 l).length = l.length.choose 0

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
⊢ length.{u} (α := List α) (sublistsLen (n + 1) []) = (length.{u} (α := α) []).choose (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
rw : (sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
rw₁ : (sublistsLen (n + 1) l).length + (map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
rw₂ : l.length.choose (n + 1) + (map (cons a) (sublistsLen n l)).length = (a :: l).length.choose (n + 1)
rw₃ : l.length.choose (n + 1) + (sublistsLen n l).length = (a :: l).length.choose (n + 1)
rw₄ : l.length.choose (n + 1) + l.length.choose n = (a :: l).length.choose (n + 1)
rw₅ : l.length.choose (n + 1) + l.length.choose n = (l.length + 1).choose (n + 1)
rw₆ : l.length.choose (n + 1) + l.length.choose n = l.length.choose n + l.length.choose n.succ
rw₇ rw₈ : l.length.choose n + l.length.choose (n + 1) = l.length.choose n + l.length.choose n.succ
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)

Tactic:
rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n + 1) l,
      length_map, length_sublistsLen n l, length_cons, Nat.choose_succ_succ, Nat.add_comm]

Premises used: List.length_cons, Nat.choose_succ_succ, List.length_append, List.sublistsLen_succ_cons, HAdd.hAdd, List.length_map, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ sublistsLen 0 l <+ l.sublists'

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
rw : sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'
⊢ sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'

Tactic:
rw [sublistsLen_succ_cons, sublists'_cons]

Premises used: List.sublists'_cons, List.sublistsLen_succ_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Tactic:
(sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Premises used: List.Sublist.map, List.Sublist.append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'

Tactic:
exact (sublistsLen_sublist_sublists' _ _).append ((sublistsLen_sublist_sublists' _ _).map _)

Premises used: List.Sublist.map, List.Sublist.append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen 0 l₁ <+ sublistsLen 0 l₂

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂

Tactic:
?_
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
succ :
  ∀ (n : ℕ) (IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂) {l₁ l₂ : List α}
    (h : l₁ <+ l₂), sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂

Tactic:
induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ Sublist.{u} (α := List α) (sublistsLen (n + 1) []) (sublistsLen (n + 1) [])

Tactic:
rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
IH : sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) l₂_1
⊢ sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) (a :: l₂_1)

Tactic:
IH.trans ?_

Premises used: List.Sublist.trans
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
IH : sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) l₂_1
succ : sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) (a :: l₂_1)
⊢ sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) (a :: l₂_1)

Tactic:
refine IH.trans ?_

Premises used: List.Sublist.trans
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
IH : sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) l₂_1
succ : sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) l₂_1 ++ map (cons a) (sublistsLen n l₂_1)
⊢ sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) (a :: l₂_1)

Tactic:
rw [sublistsLen_succ_cons]

Premises used: List.sublistsLen_succ_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α} (h : l₁ <+ l₂), sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
IH : sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) l₂_1
⊢ sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) l₂_1 ++ map (cons a) (sublistsLen n l₂_1)

Tactic:
apply sublist_append_left

Premises used: List.sublist_append_left