#min_imports can miss proof-only dependencies when moving to module system

Replacing import Mathlib with the public import list printed by #min_imports (Lean 4 / Mathlib, module system) gave 'Unknown constant LipschitzWith.uniformEquicontinuous' and 'Unknown identifier sq_sum_le_card_mul_sum_sq': two lemmas used only inside proofs (one through dot notation on a term) were not covered by the suggested imports. Fix: add plain (non-public) import Mathlib.Topology.MetricSpace.UniformConvergence / import Mathlib.Algebra.Order.Chebyshev for proof-only uses, then rebuild every downstream file. Treat #min_imports output as a starting point and let the build tell you the rest.