awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
subperm : l₁.sublists' <+~ l₂.sublists'
⊢ l₁ <+~ l₂

Tactic:
Sublist.subperm <| mem_sublists'.mp <| subperm.subset <| mem_sublists'.mpr <| .refl _

Premises used: Iff.mpr, List.mem_sublists', List.Sublist.refl, Iff.mp, List.Sublist.subperm, List.Subperm.subset
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
rw : l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
rw [sublists'_cons]

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

Tactic:
Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

Premises used: List.Perm.append, List.Perm.symm, List.sublists_perm_sublists', List.Perm.map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)

Premises used: List.Perm.append, List.Perm.symm, List.sublists_perm_sublists', List.Perm.map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse

Tactic:
rw [revzip] at h

Premises used: List.revzip
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, l₂)
⊢ l₁ = [] ∧ l₂ = []

Tactic:
simpa using h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, l₂)
⊢ l₁ = [] ∧ l₂ = []

Tactic:
have : l₁ = [] ∧ l₂ = [] := by simpa using h
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, l₂)
this : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []

Tactic:
simp [this]
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun (x : List α) ↦ x ++ [a]) l'.sublists).zip
      (reverse (map (fun (x : List α) ↦ x ++ [a]) l'.sublists) ++ l'.sublists.reverse)
⊢ l'.sublists.length = length (α := List α) (reverse (map (fun (x : List α) ↦ x ++ [a]) l'.sublists))

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse
⊢ (l₁, l₂) ∈
    map (Prod.map id fun (x : List α) ↦ x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun (x : List α) ↦ x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)

Tactic:
rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *

Premises used: List.map_reverse, List.zip_map_left, List.sublists_concat, List.zip_map_right, List.reverse_append, List.zip_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun (x : List α) ↦ x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun (x : List α) ↦ x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ (∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ a_1 ++ [a] = l₁ ∧ id b = l₂

Tactic:
simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h

Premises used: Prod.mk_inj, List.mem_append, Prod.map_apply, List.mem_map, Prod.exists
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
append_singleton :
  ∀ (l₁ l₂' : List α) (h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse), id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]
append_singleton₁ :
  ∀ (l₁' l₂ : List α) (h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁' ++ [a] ++ id l₂ ~ l' ++ [a]
⊢ l₁ ++ l₂ ~ l' ++ [a]

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

Premises used: rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
append_singleton : id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]

Tactic:
(ih _ _ h).append_right _

Premises used: List.Perm.append_right
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]

Tactic:
exact (ih _ _ h).append_right _

Premises used: List.Perm.append_right
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
append_singleton : l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Tactic:
rw [append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
append_singleton : l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]

Tactic:
apply (perm_append_comm.append_left _).trans

Premises used: List.Perm.append_left, List.Perm.trans, List.perm_append_comm
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
append_singleton : l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]

Tactic:
(ih _ _ h).append_right _

Premises used: List.Perm.append_right
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]

Tactic:
exact (ih _ _ h).append_right _

Premises used: List.Perm.append_right
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
nil :
  ∀ (l₁ l₂ : List α)
    (h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, l₂)),
    l₁ ++ l₂ ~ []
append_singleton :
  ∀ (l' : List α) (a : α) (ih : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁ ++ l₂ ~ l')
    (l₁ l₂ : List α) (h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse), l₁ ++ l₂ ~ l' ++ [a]
⊢ l₁ ++ l₂ ~ l

Tactic:
induction l using List.reverseRecOn generalizing l₁ l₂ with
  | nil =>
    have : l₁ = [] ∧ l₂ = [] := by simpa using h
    simp [this]
  | append_singleton l' a ih =>
    rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *
    simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
    · rw [← append_assoc]
      exact (ih _ _ h).append_right _
    · rw [append_assoc]
      apply (perm_append_comm.append_left _).trans
      rw [← append_assoc]
      exact (ih _ _ h).append_right _

Premises used: List.append_assoc, Prod.mk_inj, List.Perm.append_left, List.Perm.trans, List.mem_append, List.perm_append_comm, List.map_reverse, List.zip_map_left, Prod.map_apply, List.sublists_concat, List.zip_map_right, List.mem_map, Prod.exists, List.reverse_append, List.zip_append, rfl, List.nil
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse

Tactic:
rw [revzip] at h

Premises used: List.revzip
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l₁ l₂ : List α
h : Membership.mem (γ := List (List α × List α)) (zip (sublists' []) (reverse (sublists' []))) (l₁, l₂)
⊢ l₁ ++ l₂ ~ []

Tactic:
simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]

Premises used: List.mem_singleton, List.Perm.refl, List.append_nil, List.reverse_cons, Prod.mk.injEq, List.nil_append, List.sublists'_nil, List.zip_nil_right, List.reverse_nil, List.zip_cons_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
cons :
  ∀
    (h :
      (l₁, l₂) ∈
        map (Prod.map id (List.cons a)) (l.sublists'.zip l.sublists'.reverse) ++
          map (Prod.map (List.cons a) id) (l.sublists'.zip l.sublists'.reverse)),
    l₁ ++ l₂ ~ a :: l
cons₁ :
  ∀
    (h :
      (l₁, l₂) ∈
        (l.sublists' ++ map (List.cons a) l.sublists').zip
          ((map (List.cons a) l.sublists').reverse ++ l.sublists'.reverse)),
    l.sublists'.length = (map (List.cons a) l.sublists').reverse.length
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *

Premises used: List.sublists'_cons, List.map_reverse, List.zip_map_left, List.zip_map_right, List.reverse_append, List.zip_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id (cons a)) (l.sublists'.zip l.sublists'.reverse) ++
      map (Prod.map (cons a) id) (l.sublists'.zip l.sublists'.reverse)
⊢ (∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l.sublists'.zip l.sublists'.reverse ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ (a_1 : List α), (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁

Tactic:
simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h

Premises used: exists_eq_right_right, List.mem_append, Prod.mk.injEq, Prod.map_apply, List.mem_map, Prod.exists, id_eq
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l.sublists' ++ map (cons a) l.sublists').zip ((map (cons a) l.sublists').reverse ++ l.sublists'.reverse)
⊢ l.sublists'.length = (map (cons a) l.sublists').reverse.length

Tactic:
simp
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
⊢ (∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l.sublists'.zip l.sublists'.reverse ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ (a_1 : List α), (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁

Tactic:
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
      <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h; simp]

Premises used: exists_eq_right_right, List.sublists'_cons, List.mem_append, List.map_reverse, Prod.mk.injEq, List.zip_map_left, Prod.map_apply, List.zip_map_right, List.mem_map, Prod.exists, List.reverse_append, List.zip_append, id_eq
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (∃ (a_1 : List α), ∃ (b : List α), (a_1, b) ∈ l.sublists'.zip l.sublists'.reverse ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ (a_1 : List α), (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁
cons : ∀ (l₁ l₂' : List α) (h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ a :: l₂' ~ a :: l
cons₁ : ∀ (l₁' : List α) (h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse), a :: l₁' ++ l₂ ~ a :: l
⊢ l₁ ++ l₂ ~ a :: l

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

Premises used: rfl
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ a :: l₂' ~ a :: l

Tactic:
perm_middle.trans ((IH _ _ h).cons _)

Premises used: List.Perm.cons, List.Perm.trans, List.perm_middle
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ a :: l₂' ~ a :: l

Tactic:
exact perm_middle.trans ((IH _ _ h).cons _)

Premises used: List.Perm.cons, List.Perm.trans, List.perm_middle
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ a :: l₁' ++ l₂ ~ a :: l

Tactic:
(IH _ _ h).cons _

Premises used: List.Perm.cons, List.append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ a :: l₁' ++ l₂ ~ a :: l

Tactic:
exact (IH _ _ h).cons _

Premises used: List.Perm.cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
nil :
  ∀ (l₁ l₂ : List α)
    (h : Membership.mem (γ := List (List α × List α)) (zip (sublists' []) (reverse (sublists' []))) (l₁, l₂)),
    l₁ ++ l₂ ~ []
cons :
  ∀ (a : α) (l : List α) (IH : ∀ (l₁ l₂ : List α) (h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ l₂ ~ l)
    (l₁ l₂ : List α) (h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse), l₁ ++ l₂ ~ a :: l
⊢ l₁ ++ l₂ ~ l

Tactic:
induction l generalizing l₁ l₂ with
  | nil =>
    simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]
  | cons a l IH =>
    rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
      <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h; simp]
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
    · exact perm_middle.trans ((IH _ _ h).cons _)
    · exact (IH _ _ h).cons _

Premises used: exists_eq_right_right, List.sublists'_cons, List.mem_singleton, List.Perm.refl, List.append_nil, List.cons, List.reverse_cons, List.mem_append, List.map_reverse, Prod.mk.injEq, List.nil_append, List.zip_map_left, Prod.map_apply, List.zip_map_right, List.sublists'_nil, List.mem_map, Prod.exists, List.zip_nil_right, List.reverse_append, List.zip_append, List.reverse_nil, rfl, id_eq, List.nil, List.zip_cons_cons
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
⊢ Perm.{u} (α := List α) (flatMap (fun (n : ℕ) ↦ sublistsLen n []) (range (length.{u} (α := α) [] + 1))) (sublists' [])

Tactic:
simp [range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
cons :
  [] :: flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl ++ map (List.cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Tactic:
simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]

Premises used: List.sublists'_cons, List.sublistsLen_succ_cons, List.range_succ_eq_map, List.flatMap_cons, List.singleton_append, List.flatMap_map, List.length, List.sublistsLen_zero
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl ++ map (cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_

Premises used: List.flatMap_append_perm, List.Perm.cons, List.range, List.Perm.trans, HAdd.hAdd, List.Perm.symm, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
cons :
  [] ::
      HAppend.hAppend (α := List (List α)) (flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)))
        (flatMap (fun (a : ℕ) ↦ map (List.cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'
⊢ [] :: flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl ++ map (List.cons h) (sublistsLen a tl)) (range (tl.length + 1)) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'

Tactic:
refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_

Premises used: List.flatMap_append_perm, List.Perm.cons, List.range, List.Perm.trans, HAdd.hAdd, List.Perm.symm, OfNat.ofNat, List.length
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
cons :
  [] :: flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (List.cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'
⊢ [] ::
      HAppend.hAppend (α := List (List α)) (flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)))
        (flatMap (fun (a : ℕ) ↦ map (List.cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'

Tactic:
simp_rw [← List.map_flatMap, ← cons_append]

Premises used: List.map_flatMap, List.cons_append
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
cons :
  sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (List.cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'
⊢ [] :: flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (List.cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'

Tactic:
rw [← List.singleton_append, ← List.sublistsLen_zero tl]

Premises used: List.singleton_append, List.sublistsLen_zero
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
Perm.append ?_ (l_ih.map _)

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
cons : sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (List.cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (List.cons h) tl.sublists'

Tactic:
refine Perm.append ?_ (l_ih.map _)

Premises used: List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih cons : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]

Premises used: Nat.lt_succ_self, List.sublistsLen, List.range_succ_eq_map, List.append_nil, List.flatMap_cons, List.sublistsLen_of_length_lt, List.flatMap_map, List.flatMap_singleton, Nat.succ, List.flatMap_append, List.range_succ
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
l_ih
-- Module: Mathlib.Data.List.Sublists
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
exact l_ih