case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
rcases h with ⟨C, hC⟩
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < max C 1 / ↑n ^ p
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ C _h₀, ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < C / ↑x_1 ^ p) →
      1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < max C 1 / ↑x_1 ^ p
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < max C 1 / ↑n ^ p
refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < max C 1 / ↑n ^ p
case intro
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < C / ↑x_1 ^ p) →
      1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < max C 1 / ↑x_1 ^ p
rintro n ⟨hle, m, hne, hlt⟩
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ max C 1 / ↑n ^ p
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < max C 1 / ↑n ^ p
refine ⟨hle, m, hne, hlt.trans_le ?_⟩
no goals
case intro.intro.intro.intro
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ C / ↑n ^ p ≤ max C 1 / ↑n ^ p
exact div_le_div_of_le (rpow_nonneg_of_nonneg n.cast_nonneg _) (le_max_left _ _)