-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem neg (h : LiouvilleWith p x) : LiouvilleWith p (-x)

Proof state:
case intro.intro.intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ |-x - ↑m / ↑n| < C / ↑n ^ p

Tactic:
refine ⟨-m, by simp [neg_div, hne], ?_⟩

Result:
case intro.intro.intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| < C / ↑n ^ p

Proof state:
case intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (-x)

Tactic:
refine ⟨C, hC.mono ?_⟩

Result:
case intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p

Proof state:
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -x ≠ ↑(-m) / ↑n

Tactic:
simp [neg_div, hne]

Result:
no goals

Proof state:
p x : ℝ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)

Tactic:
rcases h with ⟨C, hC⟩

Result:
case intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ LiouvilleWith p (-x)

Proof state:
case intro.intro.intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| < C / ↑n ^ p

Tactic:
convert hlt using 1

Result:
case h.e'_3
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| = |x - ↑m / ↑n|

Proof state:
case h.e'_3
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |↑(-m) / ↑n - -x| = |x - ↑m / ↑n|

Tactic:
congr! 1

Result:
case h.e'_3.h.e'_4
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n

Proof state:
case h.e'_3.h.e'_4
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3.h.e'_4
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ↑(-m) / ↑n - -x = x - ↑m / ↑n

Tactic:
push_cast

Result:
case h.e'_3.h.e'_4
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ -↑m / ↑n - -x = x - ↑m / ↑n

Proof state:
case h.e'_3
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |-x - ↑(-m) / ↑n| = |x - ↑m / ↑n|

Tactic:
rw [abs_sub_comm]

Result:
case h.e'_3
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ |↑(-m) / ↑n - -x| = |x - ↑m / ↑n|

Proof state:
case intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, -x ≠ ↑m / ↑x_1 ∧ |-x - ↑m / ↑x_1| < C / ↑x_1 ^ p

Tactic:
rintro n ⟨m, hne, hlt⟩

Result:
case intro.intro.intro
p x C : ℝ
hC : ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
⊢ ∃ m, -x ≠ ↑m / ↑n ∧ |-x - ↑m / ↑n| < C / ↑n ^ p