rcases hor with (hpos | hneg)
case h.mpr
x : ℝ
hor : x = Real.sqrt 17 ∨ x = -Real.sqrt 17
⊢ x ^ 2 = 17
case h.mpr.inl
x : ℝ
hpos : x = Real.sqrt 17
⊢ x ^ 2 = 17

case h.mpr.inr
x : ℝ
hneg : x = -Real.sqrt 17
⊢ x ^ 2 = 17