[GOAL]
m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable fun i => 1 / m ^ (i + (k + 1))!
[PROOFSTEP]
convert (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)
[GOAL]
m : ℝ
hm : 1 < m
k x✝ : ℕ
⊢ 0 ≤ 1 / m ^ (x✝ + (k + 1))!
[PROOFSTEP]
positivity
[GOAL]
m : ℝ
hm : 1 < m
k : ℕ
⊢ 0 < 1 / m ^ (0 + (k + 1))!
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ ∑' (i : ℕ), 1 / m ^ (i + (n + 1)!) = ∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!)
[PROOFSTEP]
simp only [pow_add, one_div, mul_inv, inv_pow]
  -- factor the constant `(1 / m ^ (n + 1)!)` out of the series
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
[PROOFSTEP]
rw [tsum_geometric_of_lt_1 (by positivity) mi]
[GOAL]
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ 0 ≤ 1 / m
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 ≤ 1 / m ^ (n + 1)!
[PROOFSTEP]
positivity
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / m ^ (n ! * n)
[PROOFSTEP]
apply (div_le_div_iff _ _).mpr
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ 1 * m ^ (n ! * (n + 1))
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
conv_rhs =>
  rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
    -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
| 1 * m ^ (n ! * (n + 1))
[PROOFSTEP]
rw [one_mul, mul_add, pow_add, mul_one, pow_mul, mul_comm, ← pow_mul]
  -- the second factors coincide, so we prove the inequality of the first factors*
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 * m ^ (n ! * n) ≤ m ^ n ! * m ^ (n ! * n)
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
refine'
  (mul_le_mul_right _).mpr
    _
      -- solve all the inequalities `0 < m ^ ??`
[GOAL]
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
n : ℕ m : ℝ hm : 2 ≤ m ⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
any_goals
  exact
    pow_pos (zero_lt_two.trans_le hm)
      _
        -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_1
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)
[PROOFSTEP]
exact
  pow_pos (zero_lt_two.trans_le hm)
    _
      -- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
[GOAL]
case refine'_2
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !
[PROOFSTEP]
exact _root_.trans (_root_.trans hm (pow_one _).symm.le) (pow_mono (one_le_two.trans hm) n.factorial_pos)
[GOAL]
m : ℕ
hm : 0 < m
k : ℕ
⊢ ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
[PROOFSTEP]
induction' k with k h
[GOAL]
case zero
m : ℕ
hm : 0 < m
⊢ ∃ p, partialSum (↑m) Nat.zero = ↑p / ↑(m ^ Nat.zero !)
[PROOFSTEP]
exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]⟩
[GOAL]
m : ℕ
hm : 0 < m
⊢ partialSum (↑m) Nat.zero = ↑1 / ↑(m ^ Nat.zero !)
[PROOFSTEP]
rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]
[GOAL]
case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
rcases h with ⟨p_k, h_k⟩
[GOAL]
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
use p_k * m ^ ((k + 1)! - k !) + 1
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (Nat.succ k) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (Nat.succ k)!)
[PROOFSTEP]
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (Nat.succ k)!) + ↑(m ^ k !) * 1 * ↑(m ^ (Nat.succ k)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)
[PROOFSTEP]
norm_cast
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (Nat.succ k)! + m ^ k ! * 1 * m ^ (Nat.succ k)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
[PROOFSTEP]
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
[GOAL]
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0
case h.hd m : ℕ hm : 0 < m k p_k : ℕ h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !) ⊢ ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
all_goals positivity
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
[PROOFSTEP]
positivity
[GOAL]
m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
have mZ1 : 1 < (m : ℤ) := by norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
⊢ 1 < ↑m
[PROOFSTEP]
norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
have m1 : 1 < (m : ℝ) := by norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
⊢ 1 < ↑m
[PROOFSTEP]
norm_cast
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
⊢ Liouville (liouvilleNumber ↑m)
[PROOFSTEP]
intro n
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n : ℕ
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ ∃ a b, 1 < b ∧ liouvilleNumber ↑m ≠ ↑a / ↑b ∧ |liouvilleNumber ↑m - ↑a / ↑b| < 1 / ↑b ^ n
[PROOFSTEP]
refine' ⟨p, m ^ n !, by rw [Nat.cast_pow]; exact one_lt_pow mZ1 n.factorial_ne_zero, _⟩
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑(m ^ n !)
[PROOFSTEP]
rw [Nat.cast_pow]
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ 1 < ↑m ^ n !
[PROOFSTEP]
exact one_lt_pow mZ1 n.factorial_ne_zero
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑↑p / ↑↑(m ^ n !) ∧ |liouvilleNumber ↑m - ↑↑p / ↑↑(m ^ n !)| < 1 / ↑↑(m ^ n !) ^ n
[PROOFSTEP]
push_cast
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑(m ^ n !)
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
rw [Nat.cast_pow] at hp
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
rw [← partialSum_add_remainder m1 n, ← hp]
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
have hpos := remainder_pos m1 n
[GOAL]
case intro
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ partialSum (↑m) n + remainder (↑m) n ≠ partialSum (↑m) n ∧
    |partialSum (↑m) n + remainder (↑m) n - partialSum (↑m) n| < 1 / (↑m ^ n !) ^ n
[PROOFSTEP]
simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)
[GOAL]
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
hpos : 0 < remainder (↑m) n
⊢ 2 ≤ ↑m
[PROOFSTEP]
assumption_mod_cast


[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