rw [heq12, add_le_add_iff_right, sq_le_sq, abs_of_pos (by simp), le_abs, le_neg] at h12le
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
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