have heq12 : (12 : ℝ) = (3^2) + 3 := by ring
case h.mp.intro
x : ℝ
h12le : 12 ≤ x ^ 2 + 3
h19ge : 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
heq12 : 12 = 3 ^ 2 + 3
⊢ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3