use Set.Ioo (Sup.sup a c) (Inf.inf b d)
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
case h
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
c d : ℝ
hcd : Set.Ioo c d = I2
⊢ Set.Ioo (a ⊔ c) (b ⊓ d) ∈ open_intervals ∧ x ∈ Set.Ioo (a ⊔ c) (b ⊓ d) ∧ Set.Ioo (a ⊔ c) (b ⊓ d) ⊆ I1 ∩ I2