no goals
α : Type u_1
β : Type u_2
γ : Type ?u.428121
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
classical
  refine' ⟨fun h => le_iff_count.mpr fun a => _, map_le_map⟩
  simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)
α : Type u_1
β : Type u_2
γ : Type ?u.428121
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
α : Type u_1
β : Type u_2
γ : Type ?u.428121
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t
refine' ⟨fun h => le_iff_count.mpr fun a => _, map_le_map⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.428121
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)