[GOAL]
⊢ Dense {x | Irrational x}
[PROOFSTEP]
refine' Real.isTopologicalBasis_Ioo_rat.dense_iff.2 _
[GOAL]
⊢ ∀ (o : Set ℝ), o ∈ ⋃ (a : ℚ) (b : ℚ) (_ : a < b), {Ioo ↑a ↑b} → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
[PROOFSTEP]
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]
[GOAL]
⊢ ∀ (o : Set ℝ) (x x_1 : ℚ), x < x_1 → o = Ioo ↑x ↑x_1 → Set.Nonempty o → Set.Nonempty (o ∩ {x | Irrational x})
[PROOFSTEP]
rintro _ a b hlt rfl _
[GOAL]
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty (Ioo ↑a ↑b ∩ {x | Irrational x})
[PROOFSTEP]
rw [inter_comm]
[GOAL]
a b : ℚ
hlt : a < b
a✝ : Set.Nonempty (Ioo ↑a ↑b)
⊢ Set.Nonempty ({x | Irrational x} ∩ Ioo ↑a ↑b)
[PROOFSTEP]
exact exists_irrational_btwn (Rat.cast_lt.2 hlt)
[GOAL]
x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ { val := x, property := hx } < { val := x + ↑1, property := (_ : Irrational (x + ↑1)) }
[PROOFSTEP]
simp
[GOAL]
x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ { val := x - ↑1, property := (_ : Irrational (x - ↑1)) } < { val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
have A : IsClosed (range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ)) :=
  ((isClosedMap_smul₀ (n⁻¹ : ℝ)).comp Int.closedEmbedding_coe_real.isClosedMap).closed_range
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
have B : x ∉ range (fun m => (n : ℝ)⁻¹ * m : ℤ → ℝ) :=
  by
  rintro ⟨m, rfl⟩
  simp at hx 
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
⊢ ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
m : ℤ
hx : Irrational ((fun m => (↑n)⁻¹ * ↑m) m)
⊢ False
[PROOFSTEP]
simp at hx 
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
[PROOFSTEP]
refine' (ge_mem_nhds ε0).mono fun δ hδ m => not_lt.1 fun hlt => _
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist x (↑m / ↑n) < δ
⊢ False
[PROOFSTEP]
rw [dist_comm] at hlt 
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ False
[PROOFSTEP]
refine' hε (ball_subset_ball hδ hlt) ⟨m, _⟩
[GOAL]
case intro.intro
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m => (↑n)⁻¹ * ↑m)
B : ¬x ∈ range fun m => (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m => (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ (fun m => (↑n)⁻¹ * ↑m) m = ↑m / ↑n
[PROOFSTEP]
simp [div_eq_inv_mul]
[GOAL]
x : ℝ
hx : Irrational x
n : ℕ
ε : ℝ
H : ∀ (k : ℕ), k ≤ n → ∀ (m : ℤ), ε ≤ dist x (↑m / ↑k)
r : ℚ
hr : r.den ≤ n
⊢ ε ≤ dist x ↑r
[PROOFSTEP]
simpa only [Rat.cast_def] using H r.den hr r.num
