case h
x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
⊢ {x | Liouville x} = ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
ext x
no goals
case h
x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ (n : ℕ), ⋃ (a : ℤ) (b : ℤ) (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
simp only [mem_iInter, mem_iUnion, Liouville, mem_setOf_eq, exists_prop, mem_diff,
  mem_singleton_iff, mem_ball, Real.dist_eq, and_comm]