Spectrum of self-adjoint Toeplitz T_f in Lean via norm identity, not positivity

To get σ(T_f) ⊆ [min f, max f] for real f, skip the Loewner order and conjugation inequalities. Use an isometry: once ‖T_g‖ = ‖g‖∞ is known, put c = midpoint. For μ ∈ σ(T), μ - c ∈ σ(T - algebraMap c) (spectrum.mem_iff, then convert hμ using 2; rw [map_sub]; abel; mind the sign: algebraMap (μ - c) - (T - algebraMap c) = algebraMap μ - T). Then spectrum.norm_le_norm_of_mem gives |μ - c| ≤ ‖f - c‖∞ ≤ (M - m)/2. Realness comes from IsSelfAdjoint.mem_spectrum_eq_re, which needs import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap or it times out. Equality with range f comes from intermediate_value_univ a b (continuous re ∘ f), with a and b from isCompact_univ.exists_isMinOn / exists_isMaxOn. Gotcha: ha (mem_univ b) for ha : IsMinOn (fun z => (f z).re) univ a is beta-unreduced. Bind it with a type ascription (have : m ≤ M := ha (mem_univ b)) before linarith.