English
If s ⊆ m.toEnumFinset for some Finset s of α×ℕ, then the multiset of first components s.1.map fst is ≤ m.
Русский
Если Finset s ⊆ m.toEnumFinset, тогда множество первых компонент s.1.map fst меньше либо равно m.
LaTeX
$$∀ {s : Finset (α × ℕ)}, s ⊆ m.toEnumFinset → (Multiset.map Prod.fst s.val) ≤ m$$
Lean4
@[simp]
theorem map_fst_le_of_subset_toEnumFinset {s : Finset (α × ℕ)} (hsm : s ⊆ m.toEnumFinset) : s.1.map Prod.fst ≤ m :=
by
simp_rw [le_iff_count, count_map]
rintro a
obtain ha | ha := (s.1.filter fun x ↦ a = x.1).card.eq_zero_or_pos
· rw [ha]
exact Nat.zero_le _
obtain ⟨n, han, hn⟩ : ∃ n ≥ card (s.1.filter fun x ↦ a = x.1) - 1, (a, n) ∈ s :=
by
by_contra! h
replace h : {x ∈ s | x.1 = a} ⊆ { a } ×ˢ .range (card (s.1.filter fun x ↦ a = x.1) - 1) := by
simpa +contextual [forall_swap (β := _ = a), Finset.subset_iff, imp_not_comm, not_le, Nat.lt_sub_iff_add_lt] using
h
have : card (s.1.filter fun x ↦ a = x.1) ≤ card (s.1.filter fun x ↦ a = x.1) - 1 := by
simpa [Finset.card, eq_comm] using Finset.card_mono h
cutsat
exact Nat.le_of_pred_lt (han.trans_lt <| by simpa using hsm hn)
