rcases hlege with (⟨h3le, h4ge⟩ | ⟨hm4le, hm3ge⟩)
case h.mpr
x : ℝ
hlege : 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19
case h.mpr.inl.intro
x : ℝ
h3le : 3 ≤ x
h4ge : x ≤ 4
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19

case h.mpr.inr.intro
x : ℝ
hm4le : -4 ≤ x
hm3ge : x ≤ -3
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19