simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_preimage, Set.mem_Icc, neg_le_neg_iff,
  neg_lt_neg_iff, Set.mem_union, fn]
case h
x : ℝ
⊢ x ∈ fn ⁻¹' Set.Icc 12 19 ↔ x ∈ Set.Icc 3 4 ∪ Set.Icc (-4) (-3)
case h
x : ℝ
⊢ 12 ≤ x ^ 2 + 3 ∧ x ^ 2 + 3 ≤ 19 ↔ 3 ≤ x ∧ x ≤ 4 ∨ -4 ≤ x ∧ x ≤ -3