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