obtain ⟨a, b, hab⟩ := hI1
case refine_1
I1 : Set ℝ
hI1 : I1 ∈ open_intervals
I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ open_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioo a b = I1
⊢ ∃ t₃ ∈ open_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2