mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
this : t = map (fun x ↦ i ↑x ⋯) s.attach
⊢ map (fun x ↦ f ↑x) s.attach = map g t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
f : α → γ
g : β → γ
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ (b : β), b ∈ t → ∃ a ha, i a ha = b
h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)
⊢ map f s = map g t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
⊢ l.dedup = a :: l' ↔ a ∈ l ∧ ¬a ∈ l' ∧ l.dedup.tail = l'

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.dedup = [] ↔ l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : List α
⊢ [] <+ []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : a ∈ l₁ ∪ l₂
⊢ t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ t : List α
s : t <+ l₁
e : t ++ l₂ = l₁ ∪ l₂
h : ¬a ∈ l₁ ∪ l₂
⊢ a :: t ++ l₂ = a :: l₁ ∪ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
p : α → Prop
inst✝ : DecidableEq α
⊢ (∀ (x : α), x ∈ l₁ ∪ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ xs ∪ ys = ys

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
⊢ (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l ∩ [] = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h₁ : a ∈ l₁
h₂ : a ∈ l₂
⊢ elem a l₂ = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
xs : List α
⊢ (map f xs).dedup = map f xs.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
⊢ xs ∩ ys.reverse = xs ∩ ys

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₃ : List α
h : l₂ <+ l₃
⊢ l₁ ∩ l₂ <+ l₁ ∩ l₃

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₃ : List α
h : l₁ <+ l₂
⊢ l₁ ∩ l₃ <+ l₂ ∩ l₃

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ [].bagInter l = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.bagInter [] = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
⊢ (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ count a (l₁.bagInter l₂) = min (count a l₁) (count a l₂)

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.bagInter l₂ <+ l₁

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ [a].bagInter l₁ = if a ∈ l₁ then [a] else []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ l₁
⊢ l₁.bagInter (l₂.erase a) = l₁.bagInter l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ l₂
⊢ (l₁.erase a).bagInter l₂ = l₁.bagInter l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
⊢ [].bagInter l₂ = [] ↔ [] ∩ l₂ = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : α
l₁ l₂ : List α
⊢ (b :: l₁).bagInter l₂ = [] ↔ (b :: l₁) ∩ l₂ = []

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
h : l₁.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
h : l₂.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ ∈ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ l₂.erase head✝ <+ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
⊢ l₁.bagInter l₂ <+ l₁ ∩ l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys = xs.dedup ++ ys

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ (xs ++ ys).dedup = xs.dedup ++ ys.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ l₁.bagInter t ~ l₂.bagInter t

Tactic:
induction h generalizing t with grind

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ (replicate (n + 2) x).dedup = [x]

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ l₁.bagInter t ~ l₂.bagInter t

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
⊢ count a l.dedup = if a ∈ l then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
p : l₁ ~ l₂
a : α
h : ¬a ∈ l₁
⊢ List.count a l₁.dedup = List.count a l₂.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ l.bagInter t₁ = l.bagInter t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
x✝ : α
⊢ List.count x✝ (l₁.bagInter l₂) = List.count x✝ (l₂.bagInter l₁)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk (⇑(isSetoid α)) x✝)) = if a ∈ Quot.mk (⇑(isSetoid α)) x✝ then 1 else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ≤ s.dedup ↔ s.Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
s : Multiset α
l : List α
⊢ (map f (Quot.mk (⇑(isSetoid α)) l)).dedup = map f (dedup (Quot.mk (⇑(isSetoid α)) l))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ (map f s.dedup).dedup = (map f s).dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hno : s.Nodup
⊢ s ≤ t.dedup ↔ s ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ (s + t).dedup = t.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ⊆ s
⊢ (s + t).dedup = s.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ a✝.Disjoint b✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : _root_.Disjoint s t
⊢ (s + t).dedup = s.dedup + t.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
h : t ⊆ s
⊢ (s ++ t).dedup ~ s.dedup

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
h : t₁.Disjoint t₂
⊢ l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList = [] ↔ s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.isEmpty = true ↔ s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
a : α
m : Multiset α
⊢ m.toList = [a] ↔ m = {a}

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ s.toList.length = s.card

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ s.strongInductionOn H = H s fun t _h ↦ t.strongInductionOn H

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
s : Multiset α
⊢ strongDownwardInduction H s = H s fun {t₂} ht _hst ↦ strongDownwardInduction H t₂ ht

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ s.strongDownwardInductionOn H a) = H s fun {t} ht _h ↦ t.strongDownwardInductionOn H ht

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a ↦ s.strongDownwardInductionOn H a) = H s fun {t} ht _h ↦ t.strongDownwardInductionOn H ht

Tactic:
by
  dsimp only [strongDownwardInductionOn]
  rw [strongDownwardInduction]

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : 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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
all_equal : ∀ (x y : { t // t ∈ b ∧ p t }), x = y
⊢ Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ hp =
    List.chooseX p b ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : 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:
by

Goal state after:
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
⊢ ∀ (a b : List α) (p_1 : a ≈ b),
    Eq.ndrec (motive := fun x ↦ (∃! a, a ∈ x ∧ p a) → { a // a ∈ x ∧ p a }) (fun ex_unique ↦ List.chooseX p a ⋯) ⋯ =
      fun ex_unique ↦ List.chooseX p b ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
by

Goal state after:
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : 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

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
s t : Multiset α
l₁ l₂ : List α
⊢ List.map f (l₁.diff l₂ ++ l₂) = (List.map f l₁).diff (List.map f l₂) ++ List.map f l₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ 0 ∪ s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ∪ 0 = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∪ t) = max (count a s) (count a t)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
s t : Multiset α
⊢ filter p (s ∪ t) = filter p s ∪ filter p t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∩ t ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) _l → (p x ↔ q x)
⊢ ∀ (x : α), x ∈ _l → decide (p x) = decide (q x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (b : α), p b → q b
l : List α
⊢ ∀ (a : α), decide (p a) = true → decide (q a) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : p a
⊢ decide (p a) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
x✝ : List α
h : ¬p a
⊢ ¬decide (p a) = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
_l : List α
⊢ a ∈ filter p (Quot.mk (⇑(isSetoid α)) _l) ↔ a ∈ Quot.mk (⇑(isSetoid α)) _l ∧ p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = _l ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ List.filter (fun b ↦ decide (p b)) _l = [] ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ filter (fun x ↦ True) s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ filter (fun x ↦ False) s = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
l : List α
⊢ filter p (filter q (Quot.mk (⇑(isSetoid α)) l)) = filter (fun a ↦ p a ∧ q a) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s : Multiset α
⊢ filter p (filter q s) = filter q (filter p s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ t
h₂ : s ≤ u
⊢ s ≤ t ∩ u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
x✝ : a ∈ s ∧ a ∈ t
h₁ : a ∈ s
h₂ : a ∈ t
⊢ a ∈ s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ≤ t
⊢ s ∪ t = t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∪ t + u = s + u ∪ (t + u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ s + 0 = s

Tactic:
simp only [Multiset.add_zero]

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ::ₘ (s ∪ t) = a ::ₘ s ∪ a ::ₘ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ filter p s + filter (fun a ↦ ¬p a) s = s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ∩ t + u = (s + u) ∩ (t + u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + t ∩ u = (s + t) ∩ (s + u)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
p : α → Prop
inst✝ : DecidablePred p
f : β → α
s : Multiset β
l : List β
⊢ filter p (map f (Quot.mk (⇑(isSetoid β)) l)) = map f (filter (p ∘ f) (Quot.mk (⇑(isSetoid β)) l))

Tactic:
by

Goal state after: