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
⊢ LiouvilleWith p (-x)
p q x y : ℝ
r : ℚ
m : ℤ
n : ℕ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)
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
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < C / ↑x_1 ^ p) →
      ∃ m, -x ≠ ↑m / ↑x_1 ∧ abs (-x - ↑m / ↑x_1) < C / ↑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
⊢ LiouvilleWith p (-x)
refine ⟨C, hC.mono ?_⟩
case 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 : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ abs (-x - ↑m / ↑n) < C / ↑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 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < C / ↑x_1 ^ p) →
      ∃ m, -x ≠ ↑m / ↑x_1 ∧ abs (-x - ↑m / ↑x_1) < C / ↑x_1 ^ p
rintro n ⟨m, hne, hlt⟩
case 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 : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (-x - ↑(-m) / ↑n) < C / ↑n ^ p
case 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 : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ abs (-x - ↑m / ↑n) < C / ↑n ^ p
refine ⟨-m, by simp [neg_div, hne], ?_⟩
no goals
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ -x ≠ ↑(-m) / ↑n
simp [neg_div, hne]
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (-x - ↑(-m) / ↑n) = abs (x - ↑m / ↑n)
case 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 : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (-x - ↑(-m) / ↑n) < C / ↑n ^ p
convert hlt using 1
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (↑(-m) / ↑n - -x) = abs (x - ↑m / ↑n)
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (-x - ↑(-m) / ↑n) = abs (x - ↑m / ↑n)
rw [abs_sub_comm]
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n
case h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ abs (↑(-m) / ↑n - -x) = abs (x - ↑m / ↑n)
congr! 1
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n
push_cast
no goals
case h.e'_3.h.e'_3
p q x y : ℝ
r : ℚ
m✝ : ℤ
n✝ : ℕ
C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : abs (x - ↑m / ↑n) < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n
ring