-- Mathlib/NumberTheory/Transcendental/Liouville/Residual.lean
theorem eventually_residual_liouville : ∀ᶠ x in residual ℝ, Liouville x

Proof state:
case h.e'_4.h.e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r

Tactic:
norm_cast

Result:
case h.e'_4.h.e'_3
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) ↑(r.den * 2) = r

Proof state:
⊢ ∀ᶠ (x : ℝ) in residual ℝ, Liouville x

Tactic:
rw [Filter.Eventually, setOf_liouville_eq_irrational_inter_iInter_iUnion]

Result:
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ

Proof state:
case h.e'_4.h.e'_3
r : ℚ
n : ℕ
⊢ Rat.divInt (r.num * 2) ↑(r.den * 2) = r

Tactic:
simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self]

Result:
no goals

Proof state:
case refine_1

⊢ IsGδ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
exact .iInter fun n => IsOpen.isGδ <|
      isOpen_iUnion fun a => isOpen_iUnion fun b => isOpen_iUnion fun _hb => isOpen_ball

Result:
no goals

Proof state:
case refine_2.intro.refine_2
r : ℚ
n : ℕ
⊢ ↑r ∈ ball (↑(r.num * 2) / ↑(↑r.den * 2)) (1 / ↑(↑r.den * 2) ^ n)

Tactic:
convert @mem_ball_self ℝ _ (r : ℝ) _ _

Result:
case h.e'_4.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

Proof state:
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ∈ residual ℝ

Tactic:
refine eventually_residual_irrational.and ?_

Result:
⊢ Filter.Eventually (Membership.mem (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))) (residual ℝ)

Proof state:
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n

Tactic:
refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)

Result:
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2

Proof state:
⊢ Filter.Eventually (Membership.mem (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n))) (residual ℝ)

Tactic:
refine residual_of_dense_Gδ ?_ (Rat.isDenseEmbedding_coe_real.dense.mono ?_)

Result:
case refine_1

⊢ IsGδ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

case refine_2

⊢ range Rat.cast ⊆ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Proof state:
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : 0 < r.den
⊢ 1 < ↑r.den * 2

Tactic:
omega

Result:
no goals

Proof state:
case refine_2.intro.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2

Tactic:
have := r.pos

Result:
case refine_2.intro.refine_1
r : ℚ
n : ℕ
this : 0 < r.den
⊢ 1 < ↑r.den * 2

Proof state:
case h.e'_4.h.e'_3
r : ℚ
n : ℕ
⊢ ↑(r.num * 2) / ↑(↑r.den * 2) = ↑r

Tactic:
push_cast

Result:
case h.e'_4.h.e'_3
r : ℚ
n : ℕ
⊢ ↑r.num * 2 / (↑r.den * 2) = ↑r

Proof state:
case refine_2.intro
r : ℚ
⊢ ↑r ∈ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
simp only [mem_iInter, mem_iUnion]

Result:
case refine_2.intro
r : ℚ
⊢ ↑r ∈ {x | ∀ (i : ℕ), ∃ i_1 i_2, ∃ (_ : 1 < i_2), x ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)}

Proof state:
case refine_2.intro.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < ↑r.den * 2

Tactic:
exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two

Result:
no goals

Proof state:
case refine_2.intro
r : ℚ
⊢ ↑r ∈ {x | ∀ (i : ℕ), ∃ i_1 i_2, ∃ (_ : 1 < i_2), x ∈ ball (↑i_1 / ↑i_2) (1 / ↑i_2 ^ i)}

Tactic:
refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩

Result:
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)

Proof state:
case refine_2

⊢ range Rat.cast ⊆ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
rintro _ ⟨r, rfl⟩

Result:
case refine_2.intro
r : ℚ
⊢ ↑r ∈ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}