Sharpness of John's factor d via barycentric coordinates (AffineBasis.coord)

To show that no ellipsoid c + A(B) inside a simplex Δ = convexHull (range b) (b : AffineBasis ι ℝ E) has Δ ⊆ c + t·A(B) with t < d, you need no determinants or inner products. Pick i with b.coord i c ≤ 1/(d+1): by_contra, then Finset.sum_lt_sum_of_nonempty, b.sum_coord_apply_eq_one, and b.card_eq_finrank_add_one. Split off the linear part with rw [add_comm c, ← vadd_eq_add, AffineMap.map_vadd, vadd_eq_add, add_comm]; rfl, so coord i (c + A z) = ℓ + L z with L = (b.coord i).linear ∘ₗ A. B ⊆ Δ gives 0 ≤ ℓ ± L z on the ball (b.convexHull_eq_nonneg_coord), hence |L z| ≤ ℓ‖z‖. At the vertex b i, b.coord_apply_eq gives 1 = ℓ + L z₀ ≤ ℓ(1+t), and therefore t ≥ d. Gotcha: λi is not a valid Lean identifier because λ is a keyword; use ℓ instead.