feat (Order/Interval/Finset/Floor): Relating membership of an Int or Nat cast in intervals to intervals of floor and ceil functions

[teorth]

For a FloorRing (resp. FloorSemiring) α, we relate membership of a cast ↑n in an interval
of α to membership of the integer (resp. natural number) n in the corresponding interval with
floor/ceil endpoints, for instance Int.coe_mem_Ioc_iff : ↑n ∈ Set.Ioc a b ↔ n ∈ Set.Ioc ⌊a⌋ ⌊b⌋.
If the right-hand side is finite, we express them as Finset instead.

---

AI was used to extend a small initial set of human-generated lemmas to the full set in this PR, which were then reviewed and edited by myself.

This code is placed in a new file because the core Algebra.Order.Floor files explicitly disallow the use of Finset.

[github-actions]

PR summary effbb9d950

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.Interval.Finset.Floor (new file)	662

---

Declarations diff (regex)

+ coe_mem_Ioc_iff'
++ coe_mem_Icc_iff
++ coe_mem_Ici_iff
++ coe_mem_Ico_iff
++ coe_mem_Iic_iff
++ coe_mem_Iio_iff
++ coe_mem_Ioc_iff
++ coe_mem_Ioi_iff
++ coe_mem_Ioo_iff

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit effbb9d).

• +17 new declarations
• −0 removed declarations

+Int.coe_mem_Icc_iff
+Int.coe_mem_Ici_iff
+Int.coe_mem_Ico_iff
+Int.coe_mem_Iic_iff
+Int.coe_mem_Iio_iff
+Int.coe_mem_Ioc_iff
+Int.coe_mem_Ioi_iff
+Int.coe_mem_Ioo_iff
+Nat.coe_mem_Icc_iff
+Nat.coe_mem_Ici_iff
+Nat.coe_mem_Ico_iff
+Nat.coe_mem_Iic_iff
+Nat.coe_mem_Iio_iff
+Nat.coe_mem_Ioc_iff
+Nat.coe_mem_Ioc_iff'
+Nat.coe_mem_Ioi_iff
+Nat.coe_mem_Ioo_iff

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5004	1	exposed public sections

Current commit effbb9d950
Reference commit b9a56a66c2

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

labels are []
error: the PR title should be of the form
  kind: subject
or
  kind(scope): subject
Allowed values for `kind` are [feat, chore, perf, refactor, style, fix, doc, test, ci]

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"