Lean: minimum over the unit circle, using IsLeast (range f) and building Circle elements

To prove 'min over u ∈ Circle of F(u) is m' in Mathlib, state IsLeast (Set.range fun u : Circle ↦ F u) m and read off sInf with IsLeast.csInf_eq; no BddBelow bookkeeping is needed. Build the minimizer as ⟨z, mem_sphere_zero_iff_norm.2 hz⟩ : Circle (Circle's carrier is the unit sphere), with hz : ‖z‖ = 1. Example: z = conj P / ‖P‖ via norm_div, Complex.norm_conj, Complex.norm_real. For the lower bound use Complex.re_le_norm plus Circle.norm_coe. A gotcha: in the witness goal (fun u ↦ F u) ⟨z, _⟩ = m, simp only [hd] with hd : ∀ u : Circle, F u = ... reported the argument as unused. refine (hd _).trans ?_ works.