simp only [ge_iff_le, not_le, gt_iff_lt, Set.mem_image, Set.mem_Icc, fn]
case h
x : ℝ
⊢ x ∈ fn '' Set.Icc 3 5 ↔ x ∈ Set.Icc 12 28
case h
x : ℝ
⊢ (∃ x_1, (3 ≤ x_1 ∧ x_1 ≤ 5) ∧ x_1 ^ 2 + 3 = x) ↔ 12 ≤ x ∧ x ≤ 28