awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l
⊢ f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun (x : α) ↦ f x ++ g x) l)
have cons : flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)
Tactic: refine (Perm.trans ?_ (IH.append_left _)).append_left _
-- Lean 4 proof step from Mathlib.Data.List.Perm.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
a : α
l : List α
IH : flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)
have cons : flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l
Tactic: rw [← append_assoc, ← append_assoc]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ l₁.bagInter t ~ l₂.bagInter t
have nil : ∀ (t : List α), List.bagInter [] t ~ List.bagInter [] t
Tactic: induction h generalizing t with grind
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
nil : ∀ (t : List α), List.bagInter [] t ~ List.bagInter [] t
⊢ l₁.bagInter t ~ l₂.bagInter t
have cons : ∀ (x : α) {l₁ l₂ : List α},
  l₁ ~ l₂ →
    (∀ (t : List α), l₁.bagInter t ~ l₂.bagInter t) → ∀ (t : List α), (x :: l₁).bagInter t ~ (x :: l₂).bagInter t
Tactic: induction h generalizing t with grind
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
nil : ∀ (t : List α), List.bagInter [] t ~ List.bagInter [] t
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ →
      (∀ (t : List α), l₁.bagInter t ~ l₂.bagInter t) → ∀ (t : List α), (x :: l₁).bagInter t ~ (x :: l₂).bagInter t
⊢ l₁.bagInter t ~ l₂.bagInter t
have swap : ∀ (x y : α) (l t : List α), (y :: x :: l).bagInter t ~ (x :: y :: l).bagInter t
Tactic: induction h generalizing t with grind
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
nil : ∀ (t : List α), List.bagInter [] t ~ List.bagInter [] t
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ →
      (∀ (t : List α), l₁.bagInter t ~ l₂.bagInter t) → ∀ (t : List α), (x :: l₁).bagInter t ~ (x :: l₂).bagInter t
swap : ∀ (x y : α) (l t : List α), (y :: x :: l).bagInter t ~ (x :: y :: l).bagInter t
⊢ l₁.bagInter t ~ l₂.bagInter t
have trans : ∀ {l₁ l₂ l₃ : List α},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      (∀ (t : List α), l₁.bagInter t ~ l₂.bagInter t) →
        (∀ (t : List α), l₂.bagInter t ~ l₃.bagInter t) → ∀ (t : List α), l₁.bagInter t ~ l₃.bagInter t
Tactic: induction h generalizing t with grind
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ l.bagInter t₁ = l.bagInter t₂
have cons : ∀ (a : α) (l : List α) (IH : ∀ {t₁ t₂ : List α} (p : t₁ ~ t₂), l.bagInter t₁ = l.bagInter t₂) {t₁ t₂ : List α}
  (p : t₁ ~ t₂), (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Tactic: induction l generalizing t₁ t₂ p with | nil => simp | cons a l IH => ?_
Cleared hypotheses: l, t₁, t₂, p
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α} (p : t₁ ~ t₂), l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
have pos : ∀ (h : a ∈ t₁), (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Tactic: by_cases h : a ∈ t₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α} (p : t₁ ~ t₂), l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
pos : ∀ (h : a ∈ t₁), (a :: l).bagInter t₁ = (a :: l).bagInter t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
have neg : ∀ (h : ¬a ∈ t₁), (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Tactic: by_cases h : a ∈ t₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have pos : ∀ (h₁ : x ∈ t₁), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Tactic: by_cases h₁ : x ∈ t₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
pos : ∀ (h₁ : x ∈ t₁), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have neg : ∀ (h₁ : ¬x ∈ t₁), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Tactic: by_cases h₁ : x ∈ t₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have h₂ : ¬x ∈ t₂
Tactic: have h₂ : x ∉ t₂ := h h₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have pos : ∀ (h₂ : x ∈ t₂), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Tactic: by_cases h₂ : x ∈ t₂
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
pos : ∀ (h₂ : x ∈ t₂), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have neg : ∀ (h₂ : ¬x ∈ t₂), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Tactic: by_cases h₂ : x ∈ t₂
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have pos : x :: xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
Tactic: simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l t₁ t₂ : List α
h : t₁.Disjoint t₂
⊢ l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂
have nil : [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂
Tactic: induction l with
  | nil => simp
  | cons x xs l_ih =>
    by_cases h₁ : x ∈ t₁
    · have h₂ : x ∉ t₂ := h h₁
      simp [*]
    by_cases h₂ : x ∈ t₂
    · simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih
    · simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l t₁ t₂ : List α
h : t₁.Disjoint t₂
nil : [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂
⊢ l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂
have cons : ∀ (x : α) (xs : List α) (l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂),
  (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
Tactic: induction l with
  | nil => simp
  | cons x xs l_ih =>
    by_cases h₁ : x ∈ t₁
    · have h₂ : x ∉ t₂ := h h₁
      simp [*]
    by_cases h₂ : x ∈ t₂
    · simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]
      exact perm_cons_append_cons _ l_ih
    · simp [*]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
| List.take n xs
have rw : List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
Tactic: rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.take n xs ~ List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
have conv_lhs : List.take n xs ~ List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
Tactic: conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
conv_lhs : List.take n xs ~ List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
⊢ List.take n xs ~ List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
have conv_lhs₁ : List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs ~ List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
Tactic: conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.drop n xs ~ ys ∩ List.drop n xs
have pos : ∀ (h'' : n ≤ xs.length), List.drop n xs ~ ys ∩ List.drop n xs
Tactic: by_cases h'' : n ≤ xs.length
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
pos : ∀ (h'' : n ≤ xs.length), List.drop n xs ~ ys ∩ List.drop n xs
⊢ List.drop n xs ~ ys ∩ List.drop n xs
have neg : ∀ (h'' : ¬n ≤ xs.length), List.drop n xs ~ ys ∩ List.drop n xs
Tactic: by_cases h'' : n ≤ xs.length
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ n = xs.length - n'
have rwa : n = n
Tactic: rwa [Nat.sub_sub_self]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ List.drop n xs ~ ys ∩ List.drop n xs
have h₀ : n = xs.length - n'
Tactic: have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop n xs = (List.take n' xs.reverse).reverse
have rw : List.drop n xs = (List.drop (xs.length - n') xs).reverse.reverse
Tactic: rw [take_reverse, h₀, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
rw : List.drop n xs = (List.drop (xs.length - n') xs).reverse.reverse
⊢ List.drop n xs = (List.take n' xs.reverse).reverse
have rw₁ : List.drop (xs.length - n') xs = (List.drop (xs.length - n') xs).reverse.reverse
Tactic: rw [take_reverse, h₀, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
rw : List.drop n xs = (List.drop (xs.length - n') xs).reverse.reverse
rw₁ : List.drop (xs.length - n') xs = (List.drop (xs.length - n') xs).reverse.reverse
⊢ List.drop n xs = (List.take n' xs.reverse).reverse
have rw₂ : List.drop (xs.length - n') xs = List.drop (xs.length - n') xs
Tactic: rw [take_reverse, h₀, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ List.drop n xs ~ ys ∩ List.drop n xs
have h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
Tactic: have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.drop n xs ~ ys ∩ List.drop n xs
have pos : (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse
have pos : List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse
Tactic: apply (reverse_perm _).trans
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse
have pos : List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse
Tactic: rw [inter_reverse]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse
have apply : xs.reverse ~ ys
Tactic: apply Perm.take_inter _ _ h'
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs
have simp : List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
Tactic: simp only [dropSlice_eq]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
have this : n ≤ n + m
Tactic: have : n ≤ n + m := Nat.le_add_right _ _
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
have h₂ : xs.Nodup
Tactic: have h₂ := h.nodup_iff.2 h'
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
have apply : List.take n xs ++ List.drop (n + m) xs ~ ys ∩ List.take n xs ++ ys ∩ List.drop (n + m) xs
Tactic: apply Perm.trans _ (Perm.inter_append _).symm
-- Lean 4 proof step from Mathlib.Data.List.Perm.Lattice (goal)
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
apply : List.take n xs ++ List.drop (n + m) xs ~ ys ∩ List.take n xs ++ ys ∩ List.drop (n + m) xs
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
have apply₁ : (List.take n xs).Disjoint (List.drop (n + m) xs)
Tactic: apply Perm.trans _ (Perm.inter_append _).symm
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
a : α
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
have pos : ∀ (ha : a ∈ l₁), a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
Tactic: by_cases ha : a ∈ l₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
a : α
pos : ∀ (ha : a ∈ l₁), a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
have neg : ∀ (ha : ¬a ∈ l₁), a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
Tactic: by_cases ha : a ∈ l₁
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
have refine : l₁ <+~ l₂ → ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
Tactic: refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂ : l <+ l₂
⊢ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
have obtain : ∀ (l' : List α) (h₂ : l₂ ~ l ++ l'), ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
Tactic: obtain ⟨l', h₂⟩ := h₂.exists_perm_append
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]
have mp : l <+~ [a] → l = [] ∨ l = [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l : List α
a : α
mp : l <+~ [a] → l = [] ∨ l = [a]
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]
have mpr : l = [] ∨ l = [a] → l <+~ [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l : List α
a : α
⊢ l <+~ [a] → l = [] ∨ l = [a]
have mp : (∃ (l_1 : List α), l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]
Tactic: rw [subperm_iff]
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
⊢ l = [] ∨ l = [a]
have mp : ∀ (h : l <+ [a]), l = [] ∨ l = [a]
Tactic: rwa [perm_singleton.mp hla, sublist_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
mp : ∀ (h : l <+ [a]), l = [] ∨ l = [a]
⊢ l = [] ∨ l = [a]
have mp₁ : ∀ (h : l = [] ∨ l = [a]), l = [] ∨ l = [a]
Tactic: rwa [perm_singleton.mp hla, sublist_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : map f l₁ <+~ map f l₂
⊢ l₁ <+~ l₂
have obtain : ∀ (w : List β) (perm : w ~ map f l₁) (sublist : w <+ map f l₂), l₁ <+~ l₂
Tactic: obtain ⟨w, ⟨perm, sublist⟩⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
⊢ l₁ <+~ l₂
have obtain : ∀ (x : List α) (sublistₓ : x <+ l₂) (mapₓ : w = map f x), l₁ <+~ l₂
Tactic: obtain ⟨x, ⟨sublistₓ, mapₓ⟩⟩ := sublist_map_iff.mp sublist
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ l₁ <+~ l₂
have h : x ~ l₁ ∧ x <+ l₂
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁ ∧ x <+ l₂
have h : x ~ l₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (hypothesis)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁
have perm₁ : map f x ~ map f l₁
Tactic: rw [mapₓ] at perm
Cleared hypotheses: perm, sublistₓ, mapₓ
-- Lean 4 proof step from Mathlib.Data.List.Perm.Subperm (goal)
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : l₁ <+~ l₂
⊢ map f l₁ <+~ map f l₂
have obtain : ∀ (l : List α) (hl_perm : l ~ l₁) (hl_sub : l <+ l₂), map f l₁ <+~ map f l₂
Tactic: obtain ⟨l, hl_perm, hl_sub⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd
have nil : ∀ (f : List α → β), (permutationsAux2 t ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd
Tactic: induction ys generalizing f
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
nil : ∀ (f : List α → β), (permutationsAux2 t ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd
have cons : ∀ (head : α) (tail : List α),
  (∀ (f : List α → β), (permutationsAux2 t ts [] tail f).snd ++ r = (permutationsAux2 t ts r tail f).snd) →
    ∀ (f : List α → β),
      (permutationsAux2 t ts [] (head :: tail) f).snd ++ r = (permutationsAux2 t ts r (head :: tail) f).snd
Tactic: induction ys generalizing f
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd
have nil : ∀ (f : List α → β), (permutationsAux2 t [] r [] fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
Tactic: induction ys generalizing f with
  | nil => simp
  | cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
nil :
  ∀ (f : List α → β),
    (permutationsAux2 t [] r [] fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
⊢ (permutationsAux2 t [] r ys fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd
have cons : ∀ (ys_hd : α) (tail : List α)
  (ys_ih :
    ∀ (f : List α → β),
      (permutationsAux2 t [] r tail fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r tail f).snd)
  (f : List α → β),
  (permutationsAux2 t [] r (ys_hd :: tail) fun (x : List α) ↦ f (x ++ ts)).snd =
    (permutationsAux2 t ts r (ys_hd :: tail) f).snd
Tactic: induction ys generalizing f with
  | nil => simp
  | cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]
Cleared hypotheses: ys, f
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail)) f').snd
have cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
  map g' (permutationsAux2 t ts r tail fun (x : List α) ↦ f (ys_hd :: x)).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
Tactic: simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]