α : Type u_1
β : Type ?u.20962
γ : Type ?u.20965
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
α : Type u_1
β : Type ?u.20962
γ : Type ?u.20965
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ False
refine' count_eq_zero.1 _ h
α : Type u_1
β : Type ?u.20962
γ : Type ?u.20965
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
α : Type u_1
β : Type ?u.20962
γ : Type ?u.20965
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a (s - t) = 0
rw [count_sub a s t, tsub_eq_zero_iff_le]
no goals
α : Type u_1
β : Type ?u.20962
γ : Type ?u.20965
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
a : α
s t : Multiset α
d : Nodup s
h : a ∈ s - t
h' : a ∈ t
⊢ count a s ≤ count a t
exact le_trans (nodup_iff_count_le_one.1 d _) (count_pos.2 h')