Commit 2025-03-05 14:00 a54dd1cf

chore(Topology/Instances/*Real): organize instances by class (#22562) Currently, Topology/Instances has files defining topological instances on various types, organized by the type the instance is defined on. This PR takes the E?(NN)?Real instances and organizes them instead by the class that the instance belongs to (and puts all the Real-derived types together). Restructuring in this way should hopefully allow us to work with simpler concepts while not having to define more advanced concepts at the same time. I want to make a follow-up PR reorganizing the lemmas in similar ways. This change was discussed in the comments for #22093: https://github.com/leanprover-community/mathlib4/pull/22093#issuecomment-2670785335 Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Importing.20ENNReal.20in.20normed.20groups