obtain ⟨c, d, hcd⟩ := hI2
case refine_1.intro.intro
I1 I2 : Set ℝ
hI2 : I2 ∈ upper_intervals
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
⊢ ∃ t₃ ∈ upper_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2
case refine_1.intro.intro.intro.intro
I1 I2 : Set ℝ
x : ℝ
hx : x ∈ I1 ∩ I2
a b : ℝ
hab : Set.Ioc a b = I1
c d : ℝ
hcd : Set.Ioc c d = I2
⊢ ∃ t₃ ∈ upper_intervals, x ∈ t₃ ∧ t₃ ⊆ I1 ∩ I2