awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
s : l₁_1 <+ l₂_1
IH : sublistsLen (n + 1) l₁_1 <+ sublistsLen (n + 1) l₂_1
⊢ sublistsLen (n + 1) (a :: l₁_1) <+ sublistsLen (n + 1) (a :: l₂_1)

Tactic:
simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

Premises used: List.Sublist.map, List.sublistsLen_succ_cons, List.Sublist.append
-- 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₂
succ : Sublist.{u} (α := List α) (sublistsLen (n + 1) []) (sublistsLen (n + 1) [])
succ₁ :
  ∀ {l₁ l₂ : List α} (a : α),
    l₁ <+ l₂ →
      ∀ (IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂), sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) (a :: l₂)
succ₂ :
  ∀ {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) (IH : sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂),
    sublistsLen (n + 1) (a :: l₁) <+ sublistsLen (n + 1) (a :: l₂)
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂

Tactic:
induction h with
  | slnil => rfl
  | cons a _ IH =>
    refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left
  | cons_cons a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

Premises used: List.sublistsLen_succ_cons, List.cons, List.sublist_append_left
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' : List α
h : l' ∈ sublistsLen 0 l
⊢ l'.length = 0

Tactic:
simp_all
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l' ∈ sublistsLen (n + 1) l ∨ ∃ (a_1 : List α), a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'

Tactic:
rw [sublistsLen_succ_cons, mem_append, mem_map] at h

Premises used: List.sublistsLen_succ_cons, List.mem_append, List.mem_map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l ∨ ∃ (a_1 : List α), a_1 ∈ sublistsLen n l ∧ a :: a_1 = l'
inl : ∀ (h : l' ∈ sublistsLen (n + 1) l), l'.length = n + 1
inr : ∀ (l' : List α) (h : l' ∈ sublistsLen n l), (a :: l').length = n + 1
⊢ l'.length = n + 1

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

Premises used: rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

Tactic:
length_of_sublistsLen h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) l
⊢ l'.length = n + 1

Tactic:
exact length_of_sublistsLen h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Tactic:
congr_arg (· + 1) (length_of_sublistsLen h)

Premises used: congr_arg, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen n l
⊢ (a :: l').length = n + 1

Tactic:
exact congr_arg (· + 1) (length_of_sublistsLen h)

Premises used: congr_arg, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' : List α
⊢ Membership.mem (γ := List (List α)) (sublistsLen (length.{u} (α := α) []) []) []

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
cons :
  ∀ (s : [] <+ l₂) (IH : [] ∈ sublistsLen (length.{u} (α := α) []) l₂),
    [] ∈ sublistsLen (length.{u} (α := α) []) (a :: l₂)
cons₁ :
  ∀ (b : α) (l₁ : List α) (s : b :: l₁ <+ l₂) (IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂),
    b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₂ : List α
a : α
s : [] <+ l₂
IH : [] ∈ sublistsLen (length.{u} (α := α) []) l₂
⊢ [] ∈ sublistsLen (length.{u} (α := α) []) (a :: l₂)

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
cons : b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (List.cons a) (sublistsLen l₁.length l₂)
⊢ b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]

Premises used: List.sublistsLen_succ_cons, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
mem_append_left _ IH

Premises used: List.mem_append_left
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₂ : List α
a b : α
l₁ : List α
s : b :: l₁ <+ l₂
IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂
⊢ b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
exact mem_append_left _ IH

Premises used: List.mem_append_left
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
cons_cons : a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)
⊢ a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: l₂)

Tactic:
rw [length, sublistsLen_succ_cons]

Premises used: List.sublistsLen_succ_cons, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

Premises used: Iff.mpr, And.intro, Exists.intro, List.mem_map, List.mem_append_right, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)

Tactic:
exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

Premises used: Iff.mpr, And.intro, Exists.intro, List.mem_map, List.mem_append_right, rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l' : List α
h : l' <+ l
slnil : Membership.mem (γ := List (List α)) (sublistsLen (length.{u} (α := α) []) []) []
cons :
  ∀ {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) (IH : l₁ ∈ sublistsLen l₁.length l₂), l₁ ∈ sublistsLen l₁.length (a :: l₂)
cons_cons :
  ∀ {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) (IH : l₁ ∈ sublistsLen l₁.length l₂),
    a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: l₂)
⊢ l' ∈ sublistsLen l'.length l

Tactic:
induction h with
  | slnil => simp
  | @cons l₁ l₂ a s IH =>
    rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH
  | cons_cons a s IH =>
    rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

Premises used: List.sublistsLen_succ_cons, List.cons, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l l' : List α
⊢ l' ∈ sublistsLen n l ↔ l' <+ l ∧ l'.length = n

Tactic:
⟨fun h =>
    ⟨mem_sublists'.1 ((sublistsLen_sublist_sublists' _ _).subset h), length_of_sublistsLen h⟩,
    fun ⟨h₁, h₂⟩ => h₂ ▸ mem_sublistsLen_self h₁⟩

Premises used: List.length_of_sublistsLen, Membership.mem, Eq.rec, List.sublistsLen, List.Sublist.subset, List.mem_sublistsLen_self, List.mem_sublists', And.intro, Iff.intro, Iff.mp, _private.0.List.mem_sublistsLen.match_1, List.sublistsLen_sublist_sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h : l.length < n
⊢ sublistsLen n l = []

Tactic:
eq_nil_iff_forall_not_mem.mpr fun _ =>
    mem_sublistsLen.not.mpr fun ⟨hs, hl⟩ => (h.trans_eq hl.symm).not_ge (Sublist.length_le hs)

Premises used: Iff.mpr, List.Sublist.length_le, False, List.mem_sublistsLen, Iff.not, LT.lt.trans_eq, _private.0.List.mem_sublistsLen.match_1, LT.lt.not_ge, Eq.symm, List.eq_nil_iff_forall_not_mem
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
⊢ sublistsLen (a :: l).length (a :: l) = [a :: l]

Tactic:
simp only [length, sublistsLen_succ_cons, sublistsLen_length, map,
      sublistsLen_of_length_lt (lt_succ_self _), nil_append]

Premises used: List.map, Nat.lt_succ_self, List.sublistsLen_succ_cons, List.sublistsLen_of_length_lt, List.nil_append, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
simp :
  Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R)) l.sublists' ∧
    Pairwise (fun (a_1 b : List α) ↦ Lex (swap (φ := fun (a a_2 : α) ↦ Prop) R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α),
        a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap (φ := fun (a a_4 : α) ↦ Prop) R) a_1 b
⊢ Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R)) (a :: l).sublists'

Tactic:
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]

Premises used: and_imp, List.sublists'_cons, List.pairwise_map, List.pairwise_append, List.mem_sublists', exists_imp, List.mem_map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R)) l.sublists' ∧
    Pairwise (fun (a_1 b : List α) ↦ Lex (swap (φ := fun (a a_2 : α) ↦ Prop) R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α),
        a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap (φ := fun (a a_4 : α) ↦ Prop) R) a_1 b

Tactic:
⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩

Premises used: And.intro, List.Pairwise.imp, List.Lex.cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
refine :
  ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap (φ := fun (a a_4 : α) ↦ Prop) R) a_1 b
⊢ Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R)) l.sublists' ∧
    Pairwise (fun (a_1 b : List α) ↦ Lex (swap (φ := fun (a a_2 : α) ↦ Prop) R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α),
        a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap (φ := fun (a a_4 : α) ↦ Prop) R) a_1 b

Tactic:
refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
h : l₂ <+ l
nil : ∀ (sl₁ : [] <+ l), Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) [] (a :: l₂)
cons : ∀ (b : α) (l₁ : List α) (sl₁ : b :: l₁ <+ l), Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) (b :: l₁) (a :: l₂)
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) l₁ (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
h : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) [] (a :: l₂)

Tactic:
constructor
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
h : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) (b :: l₁) (a :: l₂)

Tactic:
Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)

Premises used: List.Sublist.subset, List.Lex.rel, List.mem_cons_self
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ (a' : α), a' ∈ l → R a a'
H₂ : Pairwise R l
l₂ : List α
h : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) (b :: l₁) (a :: l₂)

Tactic:
exact Lex.rel (H₁ _ <| sl₁.subset mem_cons_self)

Premises used: List.Sublist.subset, List.Lex.rel, List.mem_cons_self
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (b a : α) ↦ R a b)) l.reverse.sublists'

Tactic:
have := (pairwise_reverse.2 H).sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
this : Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (b a : α) ↦ R a b)) l.reverse.sublists'
rwa :
  ∀ (this : Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (b a : α) ↦ R a b)) (map reverse l.sublists)),
    Pairwise (Lex R on reverse) l.sublists
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      Pairwise (fun (a b : List α) ↦ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (b a : α) ↦ R a b) a.reverse b.reverse)
        l.sublists),
    Pairwise (Lex R on reverse) l.sublists
⊢ Pairwise (Lex R on reverse) l.sublists

Tactic:
rwa [sublists'_reverse, pairwise_map] at this

Premises used: List.pairwise_map, List.sublists'_reverse
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
h_1 : l.Nodup
l₁ l₂ : List α
h : ((Lex fun (x1 x2 : α) ↦ x1 ≠ x2) on reverse) l₁ l₂
⊢ l₁ ≠ l₂

Tactic:
simpa using h.to_ne

Premises used: List.Lex.to_ne
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
rw : (map reverse l.reverse.sublists).Nodup ↔ l.Nodup
rw₁ : l.reverse.sublists.Nodup ↔ l.Nodup
rw₂ : l.reverse.Nodup ↔ l.Nodup
rw₃ rw₄ : l.Nodup ↔ l.Nodup
⊢ l.sublists'.Nodup ↔ l.Nodup

Tactic:
rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]

Premises used: List.nodup_reverse, List.sublists'_eq_sublists, List.reverse_injective, List.nodup_map_iff, List.nodup_sublists
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h_1 : l.Nodup
a b : List α
h : Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≠ x2) a b
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≠ x2) a b

Tactic:
h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h_1 : l.Nodup
a b : List α
h : Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≠ x2) a b
h₁ : ∀ (x : α), Eq.{u + 1} (α := α → Prop) (fun (x1 : α) ↦ ¬x1 = x) fun (x2 : α) ↦ x ≠ x2
⊢ Lex (fun (x1 x2 : α) ↦ x1 ≠ x2) a b

Tactic:
convert! h using 3
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h_1 : l.Nodup
a b : List α
h : Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (x1 x2 : α) ↦ x1 ≠ x2) a b
x : α
⊢ Eq.{u + 1} (α := α → Prop) (fun (x1 : α) ↦ ¬x1 = x) fun (x2 : α) ↦ x ≠ x2

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h : l.Nodup
⊢ Pairwise (fun (x1 x2 : List α) ↦ x1 ≠ x2) l.sublists'

Tactic:
have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
    (fun h => Lex.to_ne (by convert! h using 3; simp [eq_comm])) h.sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h : l.Nodup
this : Pairwise (fun (x1 x2 : List α) ↦ x1 ≠ x2) l.sublists'
⊢ (sublistsLen n l).Nodup

Tactic:
this.sublist (sublistsLen_sublist_sublists' _ _)

Premises used: List.Pairwise.sublist, List.Nodup, List.sublistsLen_sublist_sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
n : ℕ
l : List α
h : l.Nodup
this : Pairwise (fun (x1 x2 : List α) ↦ x1 ≠ x2) l.sublists'
⊢ (sublistsLen n l).Nodup

Tactic:
exact this.sublist (sublistsLen_sublist_sublists' _ _)

Premises used: List.Pairwise.sublist, List.sublistsLen_sublist_sublists'
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists = map (map f) (sublists [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
rw :
  Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) l.sublists))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) l.sublists))
⊢ (map f (a :: l)).sublists = map (map f) (a :: l).sublists

Tactic:
rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]

Premises used: List.map_cons, List.map_eq_flatMap, List.sublists_cons, List.bind_eq_flatMap
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
nil :
  Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) []))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) []))
cons :
  ∀ (head : List α) (tail : List (List α)),
    Eq.{v + 1} (α := List (List β))
        (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) tail))
        (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) tail)) →
      Eq.{v + 1} (α := List (List β))
        (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) (head :: tail)))
        (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) (head :: tail)))
⊢ Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) l.sublists))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) l.sublists))

Tactic:
induction sublists l

Premises used: List.sublists
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) []))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) []))

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
a : α
l head : List α
tail : List (List α)
tail_ih :
  Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) tail))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) tail))
⊢ Eq.{v + 1} (α := List (List β))
    (flatMap (fun (x : List β) ↦ [x, f a :: x]) (flatMap (fun (x : List α) ↦ [map f x]) (head :: tail)))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) (head :: tail)))

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
⊢ (map f []).sublists' = map (map f) (sublists' [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists' = map (map f) (a :: l).sublists'

Tactic:
simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]

Premises used: List.map_cons, Function.comp, List.sublists'_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
rw : map (map l.get) (sublists (finRange l.length)) ~ map (map l.get) (sublists' (finRange l.length))
⊢ l.sublists ~ l.sublists'

Tactic:
rw [← map_get_finRange l, sublists_map, sublists'_map]

Premises used: List.sublists'_map, List.map_get_finRange, List.sublists_map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
p : Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))
⊢ map (map l.get) (sublists (finRange l.length)) ~ map (map l.get) (sublists' (finRange l.length))

Tactic:
apply Perm.map

Premises used: List.Perm.map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
p :
  ∀ (a : List (Fin l.length)),
    Membership.mem (γ := List (List (Fin l.length))) (sublists (finRange l.length)) a ↔
      Membership.mem (γ := List (List (Fin l.length))) (sublists' (finRange l.length)) a
apply : Nodup (α := List (Fin l.length)) (sublists (finRange l.length))
apply₁ : Nodup (α := List (Fin l.length)) (sublists' (finRange l.length))
⊢ Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))

Tactic:
apply (perm_ext_iff_of_nodup _ _).mpr

Premises used: Iff.mpr, List.perm_ext_iff_of_nodup
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ ∀ (a : List (Fin l.length)),
    Membership.mem (γ := List (List (Fin l.length))) (sublists (finRange l.length)) a ↔
      Membership.mem (γ := List (List (Fin l.length))) (sublists' (finRange l.length)) a

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ Nodup (α := List (Fin l.length)) (sublists (finRange l.length))

Tactic:
nodup_sublists.mpr (nodup_finRange _)

Premises used: Iff.mpr, List.nodup_finRange, List.nodup_sublists
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ Nodup (α := List (Fin l.length)) (sublists (finRange l.length))

Tactic:
exact nodup_sublists.mpr (nodup_finRange _)

Premises used: Iff.mpr, List.nodup_finRange, List.nodup_sublists
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ Nodup (α := List (Fin l.length)) (sublists' (finRange l.length))

Tactic:
(nodup_sublists'.mpr (nodup_finRange _))

Premises used: Iff.mpr, List.nodup_sublists', List.nodup_finRange
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l : List α
⊢ Nodup (α := List (Fin l.length)) (sublists' (finRange l.length))

Tactic:
exact (nodup_sublists'.mpr (nodup_finRange _))

Premises used: Iff.mpr, List.nodup_sublists', List.nodup_finRange
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
⊢ Sublist.{u} (α := List α) (List.sublists' []) (List.sublists' [])

Tactic:
.refl _

Premises used: List.Sublist.refl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
⊢ Sublist.{u} (α := List α) (List.sublists' []) (List.sublists' [])

Tactic:
exact .refl _
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
cons : l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'
⊢ l₁_1.sublists' <+ (a :: l₂_1).sublists'

Tactic:
rw [sublists'_cons]

Premises used: List.sublists'_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
⊢ l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'

Tactic:
ih.trans (List.sublist_append_left ..)

Premises used: List.Sublist.trans, List.sublist_append_left
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
⊢ l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'

Tactic:
exact ih.trans (List.sublist_append_left ..)

Premises used: List.Sublist.trans, List.sublist_append_left
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
cons_cons : l₁_1.sublists' ++ map (List.cons a) l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'
⊢ (a :: l₁_1).sublists' <+ (a :: l₂_1).sublists'

Tactic:
rw [sublists'_cons, sublists'_cons]

Premises used: List.sublists'_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
⊢ l₁_1.sublists' ++ map (List.cons a) l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'

Tactic:
ih.append (ih.map _)

Premises used: List.Sublist.map, List.Sublist.append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
⊢ l₁_1.sublists' ++ map (List.cons a) l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'

Tactic:
exact ih.append (ih.map _)

Premises used: List.Sublist.map, List.Sublist.append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
slnil : Sublist.{u} (α := List α) (List.sublists' []) (List.sublists' [])
cons : ∀ {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → ∀ (ih : l₁.sublists' <+ l₂.sublists'), l₁.sublists' <+ (a :: l₂).sublists'
cons_cons :
  ∀ {l₁ l₂ : List α} (a : α),
    l₁ <+ l₂ → ∀ (ih : l₁.sublists' <+ l₂.sublists'), (a :: l₁).sublists' <+ (a :: l₂).sublists'
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
induction sublist with
  | slnil => exact .refl _
  | cons a _ ih =>
    rw [sublists'_cons]
    exact ih.trans (List.sublist_append_left ..)
  | cons_cons a _ ih =>
    rw [sublists'_cons, sublists'_cons]
    exact ih.append (ih.map _)

Premises used: List.sublists'_cons, List.Sublist.cons_cons, List.Sublist.slnil, List.Sublist.cons