⊢ ({x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)) ∈ residual ℝ
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x
rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]
⊢ ∀ᶠ (x : ℝ) in residual ℝ, x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
⊢ ({x | Irrational x} ∩ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)) ∈ residual ℝ
refine eventually_residual_irrational.and ?_
case refine_1

⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))

case refine_2

⊢ range Rat.cast ⊆ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
⊢ ∀ᶠ (x : ℝ) in residual ℝ, x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
refine eventually_residual.2 ⟨_, ?_, Rat.denseEmbedding_coe_real.dense.mono ?_, Subset.rfl⟩
no goals
case refine_1

⊢ IsGδ (⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))
exact isGδ_iInter fun n => IsOpen.isGδ <|
      isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball
case refine_2.intro
r : ℚ
⊢ ↑r ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
case refine_2

⊢ range Rat.cast ⊆ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
rintro _ ⟨r, rfl⟩
case refine_2.intro
r : ℚ
⊢ ∀ (i : ℕ), ∃ i_1 i_2 i_3, ↑r ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)
case refine_2.intro
r : ℚ
⊢ ↑r ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)
simp only [mem_iInter, mem_iUnion]
case refine_2.intro.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2

case refine_2.intro.refine_2
r : ℚ
n : ℕ
⊢ ↑r ∈ ball (↑(r.num * 2) / ↑(↑r.den * 2)) (1 / ↑(↑r.den * 2) ^ n)
case refine_2.intro
r : ℚ
⊢ ∀ (i : ℕ), ∃ i_1 i_2 i_3, ↑r ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : ↑(Nat.succ 0) ≤ ↑r.den
⊢ 1 < ↑r.den * 2
case refine_2.intro.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2
have := Int.ofNat_le.2 r.pos
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : 1 ≤ ↑r.den
⊢ 1 < ↑r.den * 2
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : ↑(Nat.succ 0) ≤ ↑r.den
⊢ 1 < ↑r.den * 2
rw [Int.ofNat_one] at this
no goals
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : 1 ≤ ↑r.den
⊢ 1 < ↑r.den * 2
linarith
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑(r.num * 2) / ↑(↑r.den * 2) = ↑r

case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n
case refine_2.intro.refine_2
r : ℚ
n : ℕ
⊢ ↑r ∈ ball (↑(r.num * 2) / ↑(↑r.den * 2)) (1 / ↑(↑r.den * 2) ^ n)
convert @mem_ball_self ℝ _ (r : ℝ) _ _
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑(r.num * 2) / ↑(↑r.den * 2) = ↑r
push_cast
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) ↑(r.den * 2) = r
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r
norm_cast
no goals
case h.e'_5.h.e'_3
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) ↑(r.den * 2) = r
simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self]
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n
refine' one_div_pos.2 (pow_pos (Int.cast_pos.2 _) _)
no goals
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2
exact mul_pos (Int.coe_nat_pos.2 r.pos) zero_lt_two