α : Type u_1
β : Type ?u.14144
γ : Type ?u.14147
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ max (count a s) (count a t) ≤ 1
α : Type u_1
β : Type ?u.14144
γ : Type ?u.14147
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ count a (s ∪ t) ≤ 1
rw [count_union]
no goals
α : Type u_1
β : Type ?u.14144
γ : Type ?u.14147
r : α → α → Prop
s✝ t✝ : Multiset α
a✝ : α
inst✝ : DecidableEq α
s t : Multiset α
x✝ : Nodup s ∧ Nodup t
h₁ : Nodup s
h₂ : Nodup t
a : α
⊢ max (count a s) (count a t) ≤ 1
exact max_le (nodup_iff_count_le_one.1 h₁ a) (nodup_iff_count_le_one.1 h₂ a)