awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ map (map l.get) (sublists (finRange l.length)) ~ map (map l.get) (sublists' (finRange l.length))
have p : Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))
Tactic: apply Perm.map
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))
have 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
Tactic: apply (perm_ext_iff_of_nodup _ _).mpr
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))
have apply : Nodup (α := List (Fin l.length)) (sublists (finRange l.length))
Tactic: apply (perm_ext_iff_of_nodup _ _).mpr
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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))
⊢ Perm (α := List (Fin l.length)) (sublists (finRange l.length)) (sublists' (finRange l.length))
have apply₁ : Nodup (α := List (Fin l.length)) (sublists' (finRange l.length))
Tactic: apply (perm_ext_iff_of_nodup _ _).mpr
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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' <+ (a :: l₂_1).sublists'
have cons : l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'
Tactic: rw [sublists'_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ l₁_1 l₂_1 : List α
a : α
h : l₁_1 <+ l₂_1
ih : l₁_1.sublists' <+ l₂_1.sublists'
⊢ (a :: l₁_1).sublists' <+ (a :: l₂_1).sublists'
have cons_cons : l₁_1.sublists' ++ map (List.cons a) l₁_1.sublists' <+ l₂_1.sublists' ++ map (List.cons a) l₂_1.sublists'
Tactic: rw [sublists'_cons, sublists'_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'
have slnil : Sublist.{u} (α := List α) (List.sublists' []) (List.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 _)
Cleared hypotheses: sublist
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
slnil : Sublist.{u} (α := List α) (List.sublists' []) (List.sublists' [])
⊢ l₁.sublists' <+ l₂.sublists'
have cons : ∀ {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → ∀ (ih : l₁.sublists' <+ l₂.sublists'), l₁.sublists' <+ (a :: 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 _)
Cleared hypotheses: sublist
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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'
⊢ l₁.sublists' <+ l₂.sublists'
have cons_cons : ∀ {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → ∀ (ih : l₁.sublists' <+ l₂.sublists'), (a :: l₁).sublists' <+ (a :: 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 _)
Cleared hypotheses: sublist
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
a : α
l : List α
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists
have rw : l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
Tactic: rw [sublists'_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ l₁ ++ l₂ ~ l
have h₁ : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
Tactic: rw [revzip] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
l₁ l₂ : List α
h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, l₂)
⊢ l₁ ++ l₂ ~ []
have this : l₁ = [] ∧ l₂ = []
Tactic: have : l₁ = [] ∧ l₂ = [] := by simpa using h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
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₂ ~ l' ++ [a]
have 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)
Tactic: rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
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)
⊢ l₁ ++ l₂ ~ l' ++ [a]
have 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₂
Tactic: simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂
⊢ l₁ ++ l₂ ~ l' ++ [a]
have append_singleton : ∀ (l₁ l₂' : List α) (h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse), id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]
Tactic: rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]
⊢ l₁ ++ l₂ ~ l' ++ [a]
have append_singleton₁ : ∀ (l₁' l₂ : List α) (h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse), l₁' ++ [a] ++ id l₂ ~ l' ++ [a]
Tactic: rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]
have append_singleton : id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
Tactic: rw [← append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₁' ++ [a] ++ id l₂ ~ l' ++ [a]
have append_singleton : l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
Tactic: rw [append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₁' ++ ([a] ++ id l₂) ~ l' ++ [a]
have append_singleton : l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
Tactic: apply (perm_append_comm.append_left _).trans
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]
have append_singleton : l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
Tactic: rw [← append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l
have nil : ∀ (l₁ l₂ : List α)
  (h : Membership.mem (γ := List (List α × List α)) (zip (sublists []) (reverse (sublists []))) (l₁, 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 _
Cleared hypotheses: l, l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂ ~ []
⊢ l₁ ++ l₂ ~ l
have 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]
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 _
Cleared hypotheses: l, l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ l₁ ++ l₂ ~ l
have h₁ : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
Tactic: rw [revzip] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ l₁ ++ l₂ ~ a :: l
have cons : ∀
  (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)),
  l₁ ++ l₂ ~ a :: l
Tactic: rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ l₁ ++ l₂ ~ a :: l
have 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
Tactic: rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
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)
⊢ l₁ ++ l₂ ~ a :: l
have 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₁
Tactic: simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
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
⊢ l₁ ++ l₂ ~ a :: l
have 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₁
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₁
⊢ l₁ ++ l₂ ~ a :: l
have cons : ∀ (l₁ l₂' : List α) (h : (l₁, l₂') ∈ l.sublists'.zip l.sublists'.reverse), l₁ ++ a :: l₂' ~ a :: l
Tactic: rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ l₁ ++ l₂ ~ a :: l
have cons₁ : ∀ (l₁' : List α) (h : (l₁', l₂) ∈ l.sublists'.zip l.sublists'.reverse), a :: l₁' ++ l₂ ~ a :: l
Tactic: rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
Cleared hypotheses: l₁, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ l
have nil : ∀ (l₁ l₂ : List α)
  (h : Membership.mem (γ := List (List α × List α)) (zip (sublists' []) (reverse (sublists' []))) (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 _
Cleared hypotheses: l, l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂ ~ []
⊢ l₁ ++ l₂ ~ l
have 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
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 _
Cleared hypotheses: l, l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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 (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'
have cons : [] :: 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: simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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'
have cons : [] ::
    HAppend.hAppend (α := List (List α)) (flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)))
      (flatMap (fun (a : ℕ) ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
  tl.sublists' ++ map (cons h) tl.sublists'
Tactic: refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
h : α
tl : List α
l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      HAppend.hAppend (α := List (List α)) (flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)))
        (flatMap (fun (a : ℕ) ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'
have cons : [] :: 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: simp_rw [← List.map_flatMap, ← cons_append]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun (a : ℕ) ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'
have cons : 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: rw [← List.singleton_append, ← List.sublistsLen_zero tl]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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'
have cons : sublistsLen 0 tl ++ flatMap (fun (a : ℕ) ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'
Tactic: refine Perm.append ?_ (l_ih.map _)
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n l) (range (l.length + 1)) ~ l.sublists'
have nil : Perm.{u} (α := List α) (flatMap (fun (n : ℕ) ↦ sublistsLen n []) (range (length.{u} (α := α) [] + 1))) (sublists' [])
Tactic: induction l with
  | nil => simp [range_succ]
  | cons h tl l_ih =>
    simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    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]
    exact l_ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
nil :
  Perm.{u} (α := List α) (flatMap (fun (n : ℕ) ↦ sublistsLen n []) (range (length.{u} (α := α) [] + 1))) (sublists' [])
⊢ flatMap (fun (n : ℕ) ↦ sublistsLen n l) (range (l.length + 1)) ~ l.sublists'
have cons : ∀ (h : α) (tl : List α) (l_ih : flatMap (fun (n : ℕ) ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'),
  flatMap (fun (n : ℕ) ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'
Tactic: induction l with
  | nil => simp [range_succ]
  | cons h tl l_ih =>
    simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    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]
    exact l_ih
Cleared hypotheses: l