constructor
case h.mp.intro.intro.intro
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x ∧ x ≤ 28
case h.mp.intro.intro.intro.left
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ 12 ≤ x

case h.mp.intro.intro.intro.right
x y : ℝ
hfy : y ^ 2 + 3 = x
h3le : 3 ≤ y
h5ge : y ≤ 5
⊢ x ≤ 28