have heq19 : (19 : ℝ) = (4^2) + 3 := by ring
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3
case h.mp.intro
x : ℝ
h12le : 3 ≤ x ∨ x ≤ -3
h19ge : x ^ 2 + 3 ≤ 19
heq12 : 12 = 3 ^ 2 + 3
heq19 : 19 = 4 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3