α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ toEnumFinset m₁ → p ∈ toEnumFinset m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
⊢ toEnumFinset m₁ ⊆ toEnumFinset m₂
intro p
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.snd < count p.fst m₁ → p.snd < count p.fst m₂
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p ∈ toEnumFinset m₁ → p ∈ toEnumFinset m₂
simp only [Multiset.mem_toEnumFinset]
no goals
α : Type u_1
inst✝ : DecidableEq α
m m₁ m₂ : Multiset α
h : m₁ ≤ m₂
p : α × ℕ
⊢ p.snd < count p.fst m₁ → p.snd < count p.fst m₂
exact gt_of_ge_of_gt (Multiset.le_iff_count.mp h p.1)