Commit 2025-02-15 09:16 58f3e390

refactor(Limits/Preserves/Finite): review API (#21890)

• Discard unneeded Subsingleton instances. Probably, these instances were added when the typeclasses were in Type*.
• Require a proof for Fin _ in the definition, then prove an instance for J : Type u.
• Assume Finite _ instead of Fintype _ here and there.
• Drop some no longer needed Nonempty wrappers.