-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem ne_cast_int (h : LiouvilleWith p x) (hp : 1 < p) (m : ℤ) : x ≠ m

Proof state:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False

Tactic:
rcases ((eventually_gt_atTop 0).and_frequently (h.frequently_lt_rpow_neg hp)).exists with
  ⟨n : ℕ, hn : 0 < n, m : ℤ, hne : (M : ℝ) ≠ m / n, hlt : |(M - m / n : ℝ)| < n ^ (-1 : ℝ)⟩

Result:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ False

Proof state:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|

Tactic:
have hn' : (0 : ℝ) < n := by simpa

Result:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|

Proof state:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m

Tactic:
rw [Ne, eq_div_iff hn'.ne'] at hne

Result:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬↑M * ↑n = ↑m
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m

Proof state:
p x : ℝ
h : LiouvilleWith p x
hp : 1 < p
m : ℤ
⊢ x ≠ ↑m

Tactic:
rintro rfl

Result:
p : ℝ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False

Proof state:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 / ↑n ≤ |↑M * ↑n - ↑m| / ↑n

Tactic:
gcongr

Result:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |↑M * ↑n - ↑m|

Proof state:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬↑M * ↑n = ↑m
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m

Tactic:
exact mod_cast hne

Result:
no goals

Proof state:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ 0 < ↑n

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ False

Tactic:
refine hlt.not_le ?_

Result:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|

Proof state:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ ↑n ^ (-1) ≤ |↑M - ↑m / ↑n|

Tactic:
rw [rpow_neg_one, ← one_div, sub_div' hn'.ne', abs_div, Nat.abs_cast]

Result:
case intro.intro.intro.intro
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 / ↑n ≤ |↑M * ↑n - ↑m| / ↑n

Proof state:
p : ℝ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False

Tactic:
rename' m => M

Result:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False

Proof state:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |M * ↑n - m|

Tactic:
rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Result:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ M * ↑n ≠ m

Proof state:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |↑M * ↑n - ↑m|

Tactic:
norm_cast

Result:
case intro.intro.intro.intro.hab
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 ≤ |M * ↑n - m|