no goals
α✝ : Type ?u.658802
β : Type ?u.658805
γ : Type ?u.658808
γ₂ : Type ?u.658811
δ : Type ?u.658814
ι : Sort y
s t u : Set α✝
inst✝²⁰ : TopologicalSpace α✝
inst✝¹⁹ : MeasurableSpace α✝
inst✝¹⁸ : OpensMeasurableSpace α✝
inst✝¹⁷ : TopologicalSpace β
inst✝¹⁶ : MeasurableSpace β
inst✝¹⁵ : OpensMeasurableSpace β
inst✝¹⁴ : TopologicalSpace γ
inst✝¹³ : MeasurableSpace γ
inst✝¹² : BorelSpace γ
inst✝¹¹ : TopologicalSpace γ₂
inst✝¹⁰ : MeasurableSpace γ₂
inst✝⁹ : BorelSpace γ₂
inst✝⁸ : MeasurableSpace δ
α' : Type ?u.658907
inst✝⁷ : TopologicalSpace α'
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : LinearOrder α✝
inst✝⁴ : OrderClosedTopology α✝
a b x : α✝
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ico l u = S}
simpa only [exists_prop, mem_univ, true_and_iff] using
  (@dense_univ α _).borel_eq_generateFrom_Ico_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
    mem_univ _