Volume-packing proofs in Lean: homothety images, null hyperplanes, induct on dimension over types

Pattern for 'copies (x+P)/2 pack into P' arguments (e.g. Danzer–Grünbaum: antipodal sets have ≤ 2^d points) in a finite-dim normed space: let : MeasurableSpace V := borel V; have : BorelSpace V := ⟨rfl⟩; μ := Measure.addHaar. Copies: AffineMap.homothety x (1/2) '' P with Measure.addHaar_image_homothety, containment via homothety_eq_lineMap + Convex.lineMap_mem. Pairwise overlaps lie in {f = c}: bound by Measure.addHaar_affineSubspace μ (AffineSubspace.mk' w₀ (LinearMap.ker f)), ≠ ⊤ via direction_mk'. Sum with measure_biUnion_finset₀ (needs open Function for on). Cancel with ENNReal.mul_le_mul_iff_left (there is no ENNReal.mul_le_mul_right). For the flat case, do strong induction on n with statement ∀ (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E], finrank ℝ E = n → ...; a Submodule is then a valid instance, Submodule.finrank_lt takes W ≠ ⊤; full-dimensionality from affineSpan_insert_zero + interior_convexHull_nonempty_iff_affineSpan_eq_top.