[GOAL]
⊢ {x | Liouville x} = ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
[PROOFSTEP]
simp only [mem_iInter, mem_iUnion, Liouville, mem_setOf_eq, exists_prop, mem_diff, mem_singleton_iff, mem_ball,
  Real.dist_eq, and_comm]
[GOAL]
⊢ IsGδ {x | Liouville x}
[PROOFSTEP]
rw [setOf_liouville_eq_iInter_iUnion]
[GOAL]
⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
[PROOFSTEP]
refine isGδ_iInter fun n => IsOpen.isGδ ?_
[GOAL]
n : ℕ
⊢ IsOpen (⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
[PROOFSTEP]
refine isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => ?_
[GOAL]
n : ℕ
a b : ℤ
_hb : 1 < b
⊢ IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
[PROOFSTEP]
exact isOpen_ball.inter isClosed_singleton.isOpen_compl
[GOAL]
⊢ {x | Liouville x} = {x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
refine Subset.antisymm ?_ ?_
[GOAL]
case refine_1
⊢ {x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
refine subset_inter (fun x hx => hx.irrational) ?_
[GOAL]
case refine_1
⊢ {x | Liouville x} ⊆ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
rw [setOf_liouville_eq_iInter_iUnion]
[GOAL]
case refine_1
⊢ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b} ⊆
    ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
exact iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => diff_subset _ _
[GOAL]
case refine_2
⊢ {x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}
[PROOFSTEP]
simp only [inter_iInter, inter_iUnion, setOf_liouville_eq_iInter_iUnion]
[GOAL]
case refine_2
⊢ ⋂ (i : ℕ), ⋃ (i_1 : ℤ) (i_2 : ℤ) (_ : 1 < i_2), {x | Irrational x} ∩ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i) ⊆
    ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
[PROOFSTEP]
refine iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun hb => ?_
[GOAL]
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ {x | Irrational x} ∩ ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
[PROOFSTEP]
rw [inter_comm]
[GOAL]
case refine_2
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ball (↑a / ↑b) (1 / ↑b ^ n) ∩ {x | Irrational x} ⊆ ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
[PROOFSTEP]
exact diff_subset_diff Subset.rfl (singleton_subset_iff.2 ⟨a / b, by norm_cast⟩)
[GOAL]
n : ℕ
a b : ℤ
hb : 1 < b
⊢ ↑(↑a / ↑b) = ↑a / ↑b
[PROOFSTEP]
norm_cast
[GOAL]
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x
[PROOFSTEP]
rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]
[GOAL]
⊢ {x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ
[PROOFSTEP]
refine eventually_residual_irrational.and ?_
[GOAL]
⊢ ∀ᶠ (x : ℝ) in residual ℝ, x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
refine eventually_residual.2 ⟨_, ?_, Rat.denseEmbedding_coe_real.dense.mono ?_, Subset.rfl⟩
[GOAL]
case refine_1
⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))
[PROOFSTEP]
exact
  isGδ_iInter fun n => IsOpen.isGδ <| isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball
[GOAL]
case refine_2
⊢ range Rat.cast ⊆ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
rintro _ ⟨r, rfl⟩
[GOAL]
case refine_2.intro
r : ℚ
⊢ ↑r ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
[PROOFSTEP]
simp only [mem_iInter, mem_iUnion]
[GOAL]
case refine_2.intro
r : ℚ
⊢ ∀ (i : ℕ), ∃ i_1 i_2 i_3, ↑r ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)
[PROOFSTEP]
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
[GOAL]
case refine_2.intro.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2
[PROOFSTEP]
have := Int.ofNat_le.2 r.pos
[GOAL]
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : ↑(Nat.succ 0) ≤ ↑r.den
⊢ 1 < ↑r.den * 2
[PROOFSTEP]
rw [Int.ofNat_one] at this 
[GOAL]
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : 1 ≤ ↑r.den
⊢ 1 < ↑r.den * 2
[PROOFSTEP]
linarith
[GOAL]
case refine_2.intro.refine_2
r : ℚ
n : ℕ
⊢ ↑r ∈ ball (↑(r.num * 2) / ↑(↑r.den * 2)) (1 / ↑(↑r.den * 2) ^ n)
[PROOFSTEP]
convert @mem_ball_self ℝ _ (r : ℝ) _ _
[GOAL]
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑(r.num * 2) / ↑(↑r.den * 2) = ↑r
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) ↑(r.den * 2) = r
[PROOFSTEP]
simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self]
[GOAL]
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n
[PROOFSTEP]
refine' one_div_pos.2 (pow_pos (Int.cast_pos.2 _) _)
[GOAL]
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2
[PROOFSTEP]
exact mul_pos (Int.coe_nat_pos.2 r.pos) zero_lt_two
