refine
 @TopologicalSpace.IsTopologicalBasis.mk ℝ tₗ lower_intervals ?_ ?_ rfl
⊢ TopologicalSpace.IsTopologicalBasis lower_intervals
case refine_1

⊢ ∀ t₁ ∈ lower_intervals, ∀ t₂ ∈ lower_intervals, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ lower_intervals, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2

⊢ ⋃₀ lower_intervals = Set.univ