why it reported "unknown identifier 'sqrt'"

Stream: new members

[Zihao Zhang]

import Mathlib.Data.Real.Basic

import Mathlib.Data.Real.Sqrt

section
-- 定义等式左边部分，依赖于 a, b, c

noncomputable def lhs (a b c : ℝ) : ℝ :=

  sqrt (((a ^ 3) ^ (2 / 3) + (b ^ 3) ^ (2 / 3) + (c ^ 3) ^ (2 / 3)) ^ 3 /

        ((b + 3 * a) ^ 2 + (c + 3 * b) ^ 2 + (a + 3 * c) ^ 2)) +

  5 * a ^ 3 / (a + 3 * c) + 5 * b ^ 3 / (b + 3 * a) + 5 * c ^ 3 / (c + 3 * b)
-- 标记为 noncomputable，因为 sqrt 函数涉及实数计算

noncomputable def rhs (a b c : ℝ) : ℝ :=

  sqrt (a ^ 2 + b ^ 2 + c ^ 2) /

        sqrt (10 * a ^ 2 + 10 * b ^ 2 + 10 * c ^ 2 + 6 * a * b + 6 * a * c + 6 * b * c) *

        (a ^ (1 + 1) + c ^ (1 + 1) + b ^ (1 + 1)) +

  (5 * a ^ 3 / (a + 3 * c) + 5 * b ^ 3 / (3 * a + b) + 5 * c ^ 3 / (3 * b + c))
-- 证明等式 lhs a b c = rhs a b c

theorem complex_eq (a b c : ℝ) : lhs a b c = rhs a b c :=

  sorry

end

[Ruben Van de Velde]

Because there's nothing called just sqrt - look at docs#sqrt to find half a dozen options