case a
α : Type u_2
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ count x (dedup (bind (dedup m) f)) = count x (dedup (bind m f))
α : Type u_2
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
⊢ dedup (bind (dedup m) f) = dedup (bind m f)
ext x
case a
α : Type u_2
β : Type u_1
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
case a
α : Type u_2
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ count x (dedup (bind (dedup m) f)) = count x (dedup (bind m f))
simp_rw [count_dedup]
case a
α : Type u_2
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ bind (dedup m) f ↔ x ∈ bind m f
case a
α : Type u_2
β : Type u_1
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
refine if_congr ?_ rfl rfl
no goals
case a
α : Type u_2
β : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ bind (dedup m) f ↔ x ∈ bind m f
simp