rcases hlege with ⟨h12le, h19ge⟩
case h.mp
x : ℝ
hlege : 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : x ^ 2 + 3 ≤ 19
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3