[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ count a (dedup (Quot.mk Setoid.r x✝)) = if a ∈ Quot.mk Setoid.r x✝ then 1 else 0
[PROOFSTEP]
simp only [quot_mk_to_coe'', coe_dedup, mem_coe, List.mem_dedup, coe_nodup, coe_count]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a (List.dedup x✝) = if a ∈ x✝ then 1 else 0
[PROOFSTEP]
apply List.count_dedup _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
⊢ dedup (bind (dedup m) f) = dedup (bind m f)
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ count x (dedup (bind (dedup m) f)) = count x (dedup (bind m f))
[PROOFSTEP]
simp_rw [count_dedup]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ bind (dedup m) f then 1 else 0) = if x ∈ bind m f then 1 else 0
[PROOFSTEP]
refine if_congr ?_ rfl rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ bind (dedup m) f ↔ x ∈ bind m f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
⊢ s ≤ dedup s ↔ Nodup s
[PROOFSTEP]
rw [le_dedup, and_iff_right le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Multiset α
⊢ dedup s = dedup t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
[PROOFSTEP]
simp [Nodup.ext]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ dedup (map f (dedup s)) = dedup (map f s)
[PROOFSTEP]
simp [dedup_ext]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ dedup (n • s) = dedup s
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
h : a ∈ s
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
simp [h, h0]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Multiset α
n : ℕ
h0 : n ≠ 0
a : α
h : ¬a ∈ s
⊢ count a (dedup (n • s)) = count a (dedup s)
[PROOFSTEP]
simp [h, h0]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s t : Multiset α
hno : Nodup s
⊢ s ≤ Multiset.dedup t ↔ s ≤ t
[PROOFSTEP]
simp [le_dedup, hno]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t
[PROOFSTEP]
classical
rw [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le]
simp [hn]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ n • t ↔ s ≤ t
[PROOFSTEP]
rw [← h.le_dedup_iff_le, Iff.comm, ← h.le_dedup_iff_le]
[GOAL]
α : Type u_1
s t : Multiset α
n : ℕ
h : Nodup s
hn : n ≠ 0
⊢ s ≤ Multiset.dedup t ↔ s ≤ Multiset.dedup (n • t)
[PROOFSTEP]
simp [hn]
