Theorem: countelements_le_n (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A✝ B : Set ℕ
n✝ : ℕ
A : Set ℕ
n : ℕ
⊢ countelements A n ≤ n
Tactic:
simpa [countelements] using card_filter_le (Icc 1 n) _
State after:
no goals