rw [Real.sq_sqrt]
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ Real.sqrt (x - 3) ^ 2 + 3 = x
case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ x - 3 + 3 = x

case h.right
x : ℝ
h12ge : 12 ≤ x
h28le : x ≤ 28
⊢ 0 ≤ x - 3