Order of sqrt and Real.toNNReal

Stream: mathlib4

[Niels Voss]

Which form is preferred in mathlib?

Real.toNNReal (√5)
-- or
NNReal.sqrt (Real.toNNReal 5)

Neither of them simplifies to the other, and I think the √ notation is only supported for real numbers.

[Yaël Dillies]

Surely Real.toNNReal 5 = 5?

[Yaël Dillies]

import Mathlib

example : Real.toNNReal 5 = 5 := by simp

[Niels Voss]

Sorry, 5 was meant as a placeholder, it's really an arbitrary real valued x : ℝ

[Niels Voss]

To be more specific, it is

public noncomputable def singularValues : ℕ →₀ ℝ≥0 :=
  Finsupp.embDomain Fin.valEmbedding <|
    Finsupp.ofSupportFinite
      -- TODO: Consider using `NNReal.sqrt` and pushing the coercion inside.
      (fun i ↦ Real.toNNReal √(T.isSymmetric_adjoint_comp_self.eigenvalues rfl i))
      (Set.toFinite _)

from #Is there code for X? > Singular Value Decomposition (I got permission in a DM to work on the finite-dimensional case first)