awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]) [])
⊢ Eq.{u + 1} (α := List (List α)) (sublistsLen 1 []) (map (fun (x : α) ↦ [x]) (reverse []))
have rw₂ : Eq.{u + 1} (α := List (List α)) [] []
Tactic: rw [sublistsLen_succ_nil, reverse_nil, map_nil]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun (x : α) ↦ [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun (x : α) ↦ [x]) (a :: s).reverse
have 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])
Tactic: rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw : (sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n 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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₁ : (sublistsLen (n + 1) l).length + (map (cons a) (sublistsLen n 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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₂ : l.length.choose (n + 1) + (map (cons a) (sublistsLen n 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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₃ : l.length.choose (n + 1) + (sublistsLen n 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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₄ : l.length.choose (n + 1) + l.length.choose n = (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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₅ : l.length.choose (n + 1) + l.length.choose n = (l.length + 1).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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₆ : l.length.choose (n + 1) + l.length.choose n = l.length.choose n + l.length.choose n.succ
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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ (sublistsLen (n + 1) (a :: l)).length = (a :: l).length.choose (n + 1)
have rw₇ : l.length.choose n + l.length.choose (n + 1) = l.length.choose n + l.length.choose n.succ
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]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
n : ℕ
a : α
l : List α
⊢ sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'
have rw : sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'
Tactic: rw [sublistsLen_succ_cons, sublists'_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
n : ℕ
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen n l₁ <+ sublistsLen n l₂
have 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₂
Tactic: induction n generalizing l₁ l₂ with | zero => simp | succ n IHn => ?_
Cleared hypotheses: n, l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
have succ : sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) (a :: l₂_1)
Tactic: refine IH.trans ?_
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)
have succ : sublistsLen (n + 1) l₂_1 <+ sublistsLen (n + 1) l₂_1 ++ map (cons a) (sublistsLen n l₂_1)
Tactic: rw [sublistsLen_succ_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂
have succ : Sublist.{u} (α := List α) (sublistsLen (n + 1) []) (sublistsLen (n + 1) [])
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 _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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) [])
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
have 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₂)
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 _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂)
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂
have 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₂)
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 _)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
n : ℕ
a : α
l l' : List α
h : l' ∈ sublistsLen (n + 1) (a :: l)
⊢ l'.length = n + 1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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'
⊢ l'.length = n + 1
have inl : ∀ (h : l' ∈ sublistsLen (n + 1) l), l'.length = n + 1
Tactic: rcases h with (h | ⟨l', h, rfl⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ l'.length = n + 1
have inr : ∀ (l' : List α) (h : l' ∈ sublistsLen n l), (a :: l').length = n + 1
Tactic: rcases h with (h | ⟨l', h, rfl⟩)
Cleared hypotheses: l', h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)
have cons : ∀ (s : [] <+ l₂) (IH : [] ∈ sublistsLen (length.{u} (α := α) []) l₂),
  [] ∈ sublistsLen (length.{u} (α := α) []) (a :: l₂)
Tactic: rcases l₁ with - | ⟨b, l₁⟩
Cleared hypotheses: l₁, s, IH
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂)
⊢ l₁ ∈ sublistsLen l₁.length (a :: l₂)
have cons₁ : ∀ (b : α) (l₁ : List α) (s : b :: l₁ <+ l₂) (IH : b :: l₁ ∈ sublistsLen (b :: l₁).length l₂),
  b :: l₁ ∈ sublistsLen (b :: l₁).length (a :: l₂)
Tactic: rcases l₁ with - | ⟨b, l₁⟩
Cleared hypotheses: l₁, s, IH
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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 (b :: l₁).length (a :: l₂)
have cons : b :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)
Tactic: rw [length, sublistsLen_succ_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l' l₁ l₂ : List α
a : α
s : l₁ <+ l₂
IH : l₁ ∈ sublistsLen l₁.length l₂
⊢ a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: l₂)
have cons_cons : a :: l₁ ∈ sublistsLen (l₁.length + 1) l₂ ++ map (cons a) (sublistsLen l₁.length l₂)
Tactic: rw [length, sublistsLen_succ_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen l'.length l
have slnil : Membership.mem (γ := List (List α)) (sublistsLen (length.{u} (α := α) []) []) []
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⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l l' : List α
h : l' <+ l
slnil : Membership.mem (γ := List (List α)) (sublistsLen (length.{u} (α := α) []) []) []
⊢ l' ∈ sublistsLen l'.length l
have cons : ∀ {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) (IH : l₁ ∈ sublistsLen l₁.length l₂), l₁ ∈ sublistsLen l₁.length (a :: 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⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂)
⊢ l' ∈ sublistsLen l'.length l
have cons_cons : ∀ {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) (IH : l₁ ∈ sublistsLen l₁.length l₂),
  a :: l₁ ∈ sublistsLen (a :: l₁).length (a :: 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⟩)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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)) (a :: l).sublists'
have 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
Tactic: simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
have 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
Tactic: refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) l₁ (a :: l₂)
have nil : ∀ (sl₁ : [] <+ l), Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) [] (a :: l₂)
Tactic: rcases l₁ with - | ⟨b, l₁⟩
Cleared hypotheses: l₁, sl₁
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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₂)
⊢ Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) l₁ (a :: l₂)
have cons : ∀ (b : α) (l₁ : List α) (sl₁ : b :: l₁ <+ l), Lex (swap (φ := fun (a a_1 : α) ↦ Prop) R) (b :: l₁) (a :: l₂)
Tactic: rcases l₁ with - | ⟨b, l₁⟩
Cleared hypotheses: l₁, sl₁
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
R : α → α → Prop
l : List α
H : Pairwise R l
⊢ Pairwise (Lex R on reverse) l.sublists
have this : Pairwise (Lex (swap (φ := fun (a a_1 : α) ↦ Prop) fun (b a : α) ↦ R a b)) l.reverse.sublists'
Tactic: have := (pairwise_reverse.2 H).sublists'
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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'
⊢ Pairwise (Lex R on reverse) l.sublists
have 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
Tactic: rwa [sublists'_reverse, pairwise_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ Pairwise (Lex R on reverse) l.sublists
have 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
Tactic: rwa [sublists'_reverse, pairwise_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.sublists'.Nodup ↔ l.Nodup
have rw : (map reverse l.reverse.sublists).Nodup ↔ l.Nodup
Tactic: rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
rw : (map reverse l.reverse.sublists).Nodup ↔ l.Nodup
⊢ l.sublists'.Nodup ↔ l.Nodup
have rw₁ : l.reverse.sublists.Nodup ↔ l.Nodup
Tactic: rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
rw : (map reverse l.reverse.sublists).Nodup ↔ l.Nodup
rw₁ : l.reverse.sublists.Nodup ↔ l.Nodup
⊢ l.sublists'.Nodup ↔ l.Nodup
have rw₂ : l.reverse.Nodup ↔ l.Nodup
Tactic: rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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
⊢ l.sublists'.Nodup ↔ l.Nodup
have rw₃ : l.Nodup ↔ l.Nodup
Tactic: rw [sublists'_eq_sublists, nodup_map_iff reverse_injective, nodup_sublists, nodup_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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 (fun (x1 x2 : α) ↦ x1 ≠ x2) a b
have h₁ : ∀ (x : α), Eq.{u + 1} (α := α → Prop) (fun (x1 : α) ↦ ¬x1 = x) fun (x2 : α) ↦ x ≠ x2
Tactic: convert! h using 3
-- Lean 4 proof step from Mathlib.Data.List.Sublists (hypothesis)
Goal:
α : Type u
n : ℕ
l : List α
h : l.Nodup
⊢ (sublistsLen n l).Nodup
have this : 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'
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (map f (a :: l)).sublists = map (map f) (a :: l).sublists
have 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))
Tactic: rw [map_cons, sublists_cons, bind_eq_flatMap, sublists_map f l, sublists_cons,
      bind_eq_flatMap, map_eq_flatMap, map_eq_flatMap]
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]) l.sublists))
    (flatMap (fun (x : List α) ↦ [map f x]) (flatMap (fun (x : List α) ↦ [x, a :: x]) l.sublists))
have 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]) []))
Tactic: induction sublists l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
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]) []))
⊢ 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))
have 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)))
Tactic: induction sublists l
-- Lean 4 proof step from Mathlib.Data.List.Sublists (goal)
Goal:
α : Type u
l : List α
⊢ l.sublists ~ l.sublists'
have rw : map (map l.get) (sublists (finRange l.length)) ~ map (map l.get) (sublists' (finRange l.length))
Tactic: rw [← map_get_finRange l, sublists_map, sublists'_map]