mathlib

9830a300 - chore(combinatorics/configuration): Generalize universes (#18039)

chore(combinatorics/configuration): Generalize universes (#18039) This PR generalizes the universes, allowing the `P` (points) and `L` (lines) to have different universe levels. I also switched from forall to Pi for data fields, as suggested by @alreadydone.