feat(Order/Interval/Finset): Set.ncard lemmas for LocallyFiniteOrder

[SnirBroshi]

Followup to #39414 which untagged Fintype.card_I?? as @[simp].

Adds Cardinal.mk/Set.encard/Set.ncard lemmas for the 8 interval sets Set.I?? (= 24 lemmas),
that convert them to Finset.card over the corresponding Finset.I?? from a LocallyFiniteOrder instance.

---

simp? I think it's a bit strange since the LocallyFiniteOrder instance could have crazy definitions for the finset intervals which aren't "simpler", though the instances we currently have are simple.

[github-actions]

PR summary 1e033e8e22

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.Interval.Finset.Card (new file)	751

---

Declarations diff

+ Set.cardinalMk_Icc
+ Set.cardinalMk_Ici
+ Set.cardinalMk_Ico
+ Set.cardinalMk_Ioi
+ Set.cardinalMk_Ioo
+ Set.cardinalMk_uIcc
+ Set.encard_Icc
+ Set.encard_Ici
+ Set.encard_Ico
+ Set.encard_Ioi
+ Set.encard_Ioo
+ Set.encard_uIcc
+ Set.ncard_Icc
+ Set.ncard_Ici
+ Set.ncard_Ico
+ Set.ncard_Ioi
+ Set.ncard_Ioo
+ Set.ncard_uIcc

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.