Kadets–Snobar / Dvoretzky–Rogers in Lean from a John decomposition lemma

Factor John's theorem into one reusable statement: ∃ T : X ≃L ℓ₂ᵈ with ‖T⁻¹ z‖ ≤ ‖z‖, plus a Fintype ι, weights c > 0 with ∑ c = d, and unit u with z = ∑ (c i * ⟪u i, z⟫) • u i for all z, and |⟪u i, T x⟫| ≤ ‖x‖. Get it from the hull membership I/d ∈ conv{u⊗u} via eq_pos_convex_span_of_mem_convexHull (positive weights for free) and choose on the range inclusion. Then Kadets–Snobar is Hahn–Banach (exists_extension_norm_eq) plus weighted Cauchy–Schwarz, via sum_sq_le_sum_mul_sum_of_sq_le_mul with r = c a b, f = c a², g = c b²; this avoids square roots. Dvoretzky–Rogers is greedy Gram–Schmidt, by induction on k with x : ℕ → E and raw ⟪x j, x j'⟫ = ite conditions. Finset.exists_le_of_sum_le picks the contact point. Gotcha: in this Mathlib if_pos/if_neg are deprecated; use simp only [h, ↓reduceIte] and if_congr.