use (Real.sqrt (x - 3))
case h.mpr.intro
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ ∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x
case h
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ (3 ≤ Real.sqrt (x - 3) ∧ Real.sqrt (x - 3) ≤ 5) ∧ Real.sqrt (x - 3) ^ 2 + 3 = x