α : Type u_1
β : Type u_2
γ : Type ?u.126138
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card t ≤ ↑card s
α : Type u_1
β : Type u_2
γ : Type ?u.126138
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t
refine' (map_le_map h.le).lt_of_not_le fun H => h.ne <| eq_of_le_of_card_le h.le _
α : Type u_1
β : Type u_2
γ : Type ?u.126138
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card (map f t) ≤ ↑card (map f s)
α : Type u_1
β : Type u_2
γ : Type ?u.126138
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card t ≤ ↑card s
rw [← s.card_map f, ← t.card_map f]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.126138
f : α → β
s t : Multiset α
h : s < t
H : map f t ≤ map f s
⊢ ↑card (map f t) ≤ ↑card (map f s)
exact card_le_of_le H