awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ Relation.Comp (fun (x1 : List β) (x2 : List α) ↦ x1 = map f x2) (fun (x1 x2 : List α) ↦ x1 ~ x2) (map f l) l' ↔ l ~ l'

Tactic:
simp [Relation.Comp, map_inj_right hf]

Premises used: Relation.Comp, List.map_inj_right
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
rwa : Forall₂ (fun (a : List β) (c : α) ↦ a ~ g c) (List.map f l) l
rwa₁ : Forall₂ (fun (c b : α) ↦ f c ~ g b) l l
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (x : α), x ∈ l → f x ~ g x
⊢ Forall₂ (fun (x1 x2 : List β) ↦ x1 ~ x2) (List.map f l) (List.map g l)

Tactic:
rwa [List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same]

Premises used: List.forall₂_map_right_iff, List.forall₂_map_left_iff, List.forall₂_same
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f g : α → List β
h : l₁ ~ l₂
hfg : ∀ (a : α), a ∈ l₁ → f a ~ g a
⊢ flatMap f l₁ ~ flatMap g l₂

Tactic:
.trans (.flatMap_left _ hfg) (h.flatMap_right _)

Premises used: List.Perm.trans, List.Perm.flatMap_left, List.Perm.flatMap_right
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → List β
⊢ flatMap f [] ++ flatMap g [] ~ flatMap (fun (x : α) ↦ f x ++ g x) []

Tactic:
simp
-- Module: Mathlib.Data.List.Perm.Basic
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 (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun (x : α) ↦ f x ++ g x) (a :: l)

Tactic:
?_
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
cons :
  ∀ (a : α) (l : List α) (IH : flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l),
    flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun (x : α) ↦ f x ++ g x) (a :: l)
⊢ flatMap f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x ++ g x) l

Tactic:
induction l with | nil => simp | cons a l IH => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Perm.Basic
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
cons : f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun (x : α) ↦ f x ++ g x) l)
⊢ flatMap f (a :: l) ++ flatMap g (a :: l) ~ flatMap (fun (x : α) ↦ f x ++ g x) (a :: l)

Tactic:
simp only [flatMap_cons, append_assoc]

Premises used: List.append_assoc, List.flatMap_cons
-- Module: Mathlib.Data.List.Perm.Basic
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)

Tactic:
(Perm.trans ?_ (IH.append_left _)).append_left _

Premises used: List.Perm.append_left, List.Perm.trans
-- Module: Mathlib.Data.List.Perm.Basic
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
cons : flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)
⊢ f a ++ (flatMap f l ++ (g a ++ flatMap g l)) ~ f a ++ (g a ++ flatMap (fun (x : α) ↦ f x ++ g x) l)

Tactic:
refine (Perm.trans ?_ (IH.append_left _)).append_left _

Premises used: List.Perm.append_left, List.Perm.trans
-- Module: Mathlib.Data.List.Perm.Basic
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
cons : flatMap f l ++ g a ++ flatMap g l ~ g a ++ flatMap f l ++ flatMap g l
⊢ flatMap f l ++ (g a ++ flatMap g l) ~ g a ++ (flatMap f l ++ flatMap g l)

Tactic:
rw [← append_assoc, ← append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.List.Perm.Basic
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

Tactic:
perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.List.Perm.Basic
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

Tactic:
exact perm_append_comm.append_right _

Premises used: List.perm_append_comm, List.Perm.append_right
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
g : α → List β
⊢ map f l ++ flatMap g l ~ flatMap (fun (x : α) ↦ f x :: g x) l

Tactic:
simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) g

Premises used: List.flatMap_append_perm, List.map_eq_flatMap, List.cons, List.nil
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
t₁ : List β
p : l₁ ~ l₂
⊢ l₁.product t₁ ~ l₂.product t₁

Tactic:
p.flatMap_right _

Premises used: List.product, List.Perm.flatMap_right
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l : List α
t₁ t₂ : List β
p : t₁ ~ t₂
⊢ l.product t₁ ~ l.product t₂

Tactic:
(Perm.flatMap_left _) fun _ _ => p.map _

Premises used: List.product, Prod.mk, List.Perm.flatMap_left, List.Perm.map
-- Module: Mathlib.Data.List.Perm.Basic
Goal:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
t₁ t₂ : List β
p₁ : l₁ ~ l₂
p₂ : t₁ ~ t₂
⊢ l₁.product t₁ ~ l₂.product t₂

Tactic:
(p₁.product_right t₁).trans (p₂.product_left l₂)

Premises used: List.Perm.product_left, List.Perm.trans, List.Perm.product_right
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t : List α
⊢ List.bagInter [] t ~ List.bagInter [] t

Tactic:
grind
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
x : α
l₁_1 l₂_1 : List α
h : l₁_1 ~ l₂_1
a_ih : ∀ (t : List α), l₁_1.bagInter t ~ l₂_1.bagInter t
t : List α
⊢ (x :: l₁_1).bagInter t ~ (x :: l₂_1).bagInter t

Tactic:
grind
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
x y : α
l t : List α
⊢ (y :: x :: l).bagInter t ~ (x :: y :: l).bagInter t

Tactic:
grind
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ l₁_1 l₂_1 l₃ : List α
h : l₁_1 ~ l₂_1
h_1 : l₂_1 ~ l₃
a_ih : ∀ (t : List α), l₁_1.bagInter t ~ l₂_1.bagInter t
a_ih_1 : ∀ (t : List α), l₂_1.bagInter t ~ l₃.bagInter t
t : List α
⊢ l₁_1.bagInter t ~ l₃.bagInter t

Tactic:
grind
-- Module: Mathlib.Data.List.Perm.Lattice
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
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
⊢ l₁.bagInter t ~ l₂.bagInter t

Tactic:
induction h generalizing t with grind
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ List.bagInter [] t₁ = List.bagInter [] t₂

Tactic:
simp
-- Module: Mathlib.Data.List.Perm.Lattice
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₂

Tactic:
?_
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
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₂
⊢ l.bagInter t₁ = l.bagInter t₂

Tactic:
induction l generalizing t₁ t₂ p with | nil => simp | cons a l IH => ?_

Premises used: List.Perm.cons, List.Perm.nil
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
neg : ∀ (h : ¬a ∈ t₁), (a :: l).bagInter t₁ = (a :: l).bagInter t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
by_cases h : a ∈ t₁
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
h : a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
simp [h, p.subset h, IH (p.erase _)]

Premises used: List.Perm.subset, List.Perm.erase
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
h : ¬a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
simp [h, mt p.mem_iff.2 h, IH p]

Premises used: Iff.mpr, mt, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ t₁ t₂ : List α
hl : l₁ ~ l₂
ht : t₁ ~ t₂
⊢ l₁.bagInter t₁ ~ l₂.bagInter t₂

Tactic:
ht.bagInter_left l₂ ▸ hl.bagInter_right _

Premises used: Eq.rec, List.Perm.bagInter_right, List.Perm.bagInter_left
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l₁ l₂ : List α
x : α
⊢ List.count x (l₁.bagInter l₂) = List.count x (l₂.bagInter l₁)

Tactic:
simp [List.count_bagInter, Nat.min_comm]

Premises used: Nat.min_comm, List.count_bagInter
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂

Tactic:
simp
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
neg : ∀ (h₁ : ¬x ∈ t₁), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
by_cases h₁ : x ∈ t₁
-- Module: Mathlib.Data.List.Perm.Lattice
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 ∈ t₂

Tactic:
have h₂ : x ∉ t₂ := h h₁
-- Module: Mathlib.Data.List.Perm.Lattice
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₂

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
neg : ∀ (h₂ : ¬x ∈ t₂), (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
by_cases h₂ : x ∈ t₂
-- Module: Mathlib.Data.List.Perm.Lattice
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₂
pos : x :: xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

Tactic:
simp only [*, inter_cons_of_notMem, false_or, mem_append, inter_cons_of_mem,
        not_false_iff]

Premises used: List.inter_cons_of_notMem, false_or, List.mem_append, not_false_iff, List.inter_cons_of_mem
-- Module: Mathlib.Data.List.Perm.Lattice
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₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂

Tactic:
perm_cons_append_cons _ l_ih

Premises used: List.perm_cons_append_cons
-- Module: Mathlib.Data.List.Perm.Lattice
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₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂

Tactic:
exact perm_cons_append_cons _ l_ih

Premises used: List.perm_cons_append_cons
-- Module: Mathlib.Data.List.Perm.Lattice
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₂

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
l t₁ t₂ : List α
h : t₁.Disjoint t₂
nil : [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂
cons :
  ∀ (x : α) (xs : List α) (l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂),
    (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
⊢ l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ 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 [*]

Premises used: List.inter_cons_of_notMem, List.Perm.cons, false_or, List.mem_append, not_false_iff, List.inter_cons_of_mem, List.Perm.nil
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
rw : List.filter (fun (a : α) ↦ elem a (List.take n xs)) xs
| List.take n xs

Tactic:
rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]

Premises used: Iff.mpr, List.Nodup.take_eq_filter_mem, List.Perm.nodup_iff
-- Module: Mathlib.Data.List.Perm.Lattice
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
conv_lhs₁ :
  List.filter (fun (a : α) ↦ elem a (List.take n xs)) 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

Tactic:
conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]

Premises used: Iff.mpr, List.Nodup.take_eq_filter_mem, List.Perm.nodup_iff
-- Module: Mathlib.Data.List.Perm.Lattice
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
neg : ∀ (h'' : ¬n ≤ xs.length), List.drop n xs ~ ys ∩ List.drop n xs
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
by_cases h'' : n ≤ xs.length

Premises used: List.length
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
rwa : n = n
rwa₁ : n ≤ xs.length
rwa₂ : n = n
rwa₃ rwa₄ rwa₅ : n ≤ xs.length
⊢ n = xs.length - n'

Tactic:
rwa [Nat.sub_sub_self]

Premises used: Nat.sub_sub_self
-- Module: Mathlib.Data.List.Perm.Lattice
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'

Tactic:
have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
-- Module: Mathlib.Data.List.Perm.Lattice
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
rw₂ rw₃ : List.drop (xs.length - n') xs = List.drop (xs.length - n') xs
⊢ List.drop n xs = (List.take n' xs.reverse).reverse

Tactic:
rw [take_reverse, h₀, reverse_reverse]

Premises used: List.take_reverse, List.reverse_reverse
-- Module: Mathlib.Data.List.Perm.Lattice
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

Tactic:
have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
      rw [take_reverse, h₀, reverse_reverse]
-- Module: Mathlib.Data.List.Perm.Lattice
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
pos : (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
rw [h₁]
-- Module: Mathlib.Data.List.Perm.Lattice
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
pos : List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse
⊢ (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse

Tactic:
apply (reverse_perm _).trans

Premises used: List.Perm.trans, List.reverse_perm
-- Module: Mathlib.Data.List.Perm.Lattice
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
pos : List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse
⊢ List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse

Tactic:
rw [inter_reverse]

Premises used: List.inter_reverse
-- Module: Mathlib.Data.List.Perm.Lattice
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
apply : xs.reverse ~ ys
⊢ List.take n' xs.reverse ~ ys ∩ List.take n' xs.reverse

Tactic:
apply Perm.take_inter _ _ h'

Premises used: List.Perm.take_inter
-- Module: Mathlib.Data.List.Perm.Lattice
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
apply : xs ~ ys
⊢ xs.reverse ~ ys

Tactic:
apply (reverse_perm _).trans

Premises used: List.Perm.trans, List.reverse_perm
-- Module: Mathlib.Data.List.Perm.Lattice
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
⊢ xs ~ ys

Tactic:
assumption
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
grind [drop_eq_nil_of_le]

Premises used: List.drop_eq_nil_of_le
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
simp : List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs

Tactic:
simp only [dropSlice_eq]

Premises used: List.dropSlice_eq
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ n ≤ n + m

Tactic:
have : n ≤ n + m := Nat.le_add_right _ _
-- Module: Mathlib.Data.List.Perm.Lattice
Goal:
α : Type u_1
inst : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
⊢ xs.Nodup

Tactic:
have h₂ := h.nodup_iff.2 h'
-- Module: Mathlib.Data.List.Perm.Lattice
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
apply₁ : (List.take n xs).Disjoint (List.drop (n + m) xs)
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ (List.take n xs ++ List.drop (n + m) xs)

Tactic:
apply Perm.trans _ (Perm.inter_append _).symm

Premises used: List.Perm.trans, List.Perm.inter_append, List.Perm.symm
-- Module: Mathlib.Data.List.Perm.Lattice
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 ++ ys ∩ List.drop (n + m) xs

Tactic:
Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')

Premises used: List.Perm.drop_inter, List.Perm.append, List.Perm.take_inter
-- Module: Mathlib.Data.List.Perm.Lattice
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 ++ ys ∩ List.drop (n + m) xs

Tactic:
exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')

Premises used: List.Perm.drop_inter, List.Perm.append, List.Perm.take_inter
-- Module: Mathlib.Data.List.Perm.Lattice
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).Disjoint (List.drop (n + m) xs)

Tactic:
disjoint_take_drop h₂ this

Premises used: List.disjoint_take_drop
-- Module: Mathlib.Data.List.Perm.Lattice
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).Disjoint (List.drop (n + m) xs)

Tactic:
exact disjoint_take_drop h₂ this

Premises used: List.disjoint_take_drop
-- Module: Mathlib.Data.List.Perm.Subperm
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₂
neg : ∀ (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₂

Tactic:
by_cases ha : a ∈ l₁
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
a : α
ha : a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
simp [ha, count_eq_zero_of_not_mem]

Premises used: List.count_eq_zero_of_not_mem
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ : List α
inst : DecidableEq α
a : α
ha : ¬a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
simp [ha, count_eq_zero_of_not_mem]

Premises used: List.count_eq_zero_of_not_mem
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ <+~ l₂ ↔ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l

Tactic:
⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩

Premises used: _private.0.List.subperm_iff.match_1, List.Subperm.trans, List.Perm.subperm, List.Subperm, Iff.intro, List.Sublist.subperm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ : List α
refine : l₁ <+~ l₂ → ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
⊢ l₁ <+~ l₂ ↔ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l

Tactic:
refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂ : l <+ l₂
obtain : ∀ (l' : List α) (h₂ : l₂ ~ l ++ l'), ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l
⊢ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l

Tactic:
obtain ⟨l', h₂⟩ := h₂.exists_perm_append

Premises used: List.Sublist.exists_perm_append
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂_1 : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l

Tactic:
⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

Premises used: List.prefix_append, List.Perm.trans, And.intro, Exists.intro, List.Perm.symm, List.IsPrefix.sublist, List.Perm.append_right, HAppend.hAppend
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ l : List α
h₁ : l ~ l₁
h₂_1 : l <+ l₂
l' : List α
h₂ : l₂ ~ l ++ l'
⊢ ∃ (l : List α), l ~ l₂ ∧ l₁ <+ l

Tactic:
exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩