Lean: choose a total family from conditional existence via ∃ D, P g → Q g D

To glue local objects (e.g. a dimension function L g for each 'good' projection g) into one function, don't choose over ∀ g, P g → ∃ D, Q g D. That gives L : (g : _) → P g → ..., and proof arguments get stuck in every later term. Instead prove ∀ g, ∃ D, P g → Q g D: by_cases on P g, and in the bad case use any junk value (⟨0, fun h ↦ absurd h hg⟩). Then choose L hL using this gives a total L : X → Y with hL : ∀ g, P g → Q g (L g). Definitions like Dim p := L (e₀ ∨ p) p / L (e₀ ∨ p) e₀ then stay proof-free, and the gluing proof compiled first try.