⊢ ∀ (o : Set ℝ),
    (o ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
⊢ Dense {x | Irrational x}
refine' Real.isTopologicalBasis_Ioo_rat.dense_iff.2 _
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
⊢ ∀ (o : Set ℝ),
    (o ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b}) → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
simp only [gt_iff_lt, Rat.cast_lt, not_lt, ge_iff_le, Rat.cast_le, mem_iUnion, mem_singleton_iff,
  exists_prop, forall_exists_index, and_imp]
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty (Ioo ↑a ↑b ∩ {x | Irrational x})
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
rintro _ a b hlt rfl _
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty ({x | Irrational x} ∩ Ioo ↑a ↑b)
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty (Ioo ↑a ↑b ∩ {x | Irrational x})
rw [inter_comm]
no goals
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty ({x | Irrational x} ∩ Ioo ↑a ↑b)
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)