Counting elements in a Finset

Stream: mathlib4

[Zikang Yu]

I am looking for a lemma stating that in a linearly ordered finite set, the number of elements strictly smaller than the element with index k (in the sorted sequence) is exactly k, since I have to deal with some counting problems concerning the relative positions of points and finite sets in linear orders.

The signature of this lemma should be like:

import Mathlib.Data.Finset.Sort

variable {α : Type*} [LinearOrder α] (F : Finset α) (k : Fin F.card)

theorem Finset.card_filter_lt_orderEmbOfFin : (F.filter (· < ((F.orderEmbOfFin ⋯) k))).card = k := by ...

Essentially this equation is equivalent to {i : Fin F.card | i < k}.card = {x ∈ F | x < (F.orderEmbOfFin ⋯) k}.card. And I prove it by constructing a bijection, which is quite tedious. So I wonder if there's a golfed proof or even a existing lemma.

Or maybe I should use List instead? I'm not sure.

[Zikang Yu]

I've reduced the original problem to proving {x : Fin F.card | x < k}.card = k.

I'm still struggling to find a lemma for this, even though it seems like more fundamental and obvious.

[Bhavik Mehta]

docs#Fin.card_Iio looks like it might help you here

[Zikang Yu]

That's it! Thanks.