case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : ↑(aeval x) f = 0
⊢ False
x : ℝ
lx : Liouville x
⊢ Transcendental ℤ x
rintro ⟨f : ℤ[X], f0, ef0⟩
case ef0
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : ↑(aeval x) f = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ False
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : ↑(aeval x) f = 0
⊢ False
replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0
case intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
⊢ False
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ False
obtain ⟨A, hA, h⟩ : ∃ A : ℝ, 0 < A ∧ ∀ (a : ℤ) (b : ℕ),
    (1 : ℝ) ≤ ((b : ℝ) + 1) ^ f.natDegree * (|x - a / (b + 1)| * A) :=
  exists_pos_real_of_irrational_root lx.irrational f0 ef0
case intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
⊢ False
case intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
⊢ False
rcases pow_unbounded_of_one_lt A (lt_add_one 1) with ⟨r, hn⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
⊢ False
case intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
⊢ False
obtain ⟨a, b, b1, -, a1⟩ : ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧
    |x - a / b| < 1 / (b : ℝ) ^ (r + f.natDegree) :=
  lx (r + f.natDegree)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
b0 : 0 < ↑b
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
⊢ False
have b0 : (0 : ℝ) < b := zero_lt_one.trans (by rw [← Int.cast_one]; exact Int.cast_lt.mpr b1)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < ↑b ^ natDegree f * abs (x - ↑a / ↑b)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
b0 : 0 < ↑b
⊢ False
refine' lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) _
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < ↑b ^ natDegree f * abs (x - ↑a / ↑b)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < ↑b ^ natDegree f * abs (x - ↑a / ↑b)
rw [lt_div_iff' (pow_pos b0 _), pow_add, mul_assoc] at a1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < 1 / A

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ natDegree f * abs (x - ↑a / ↑b)
case intro.intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < ↑b ^ natDegree f * abs (x - ↑a / ↑b)
refine' (_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le _
no goals
case ef0
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : ↑(aeval x) f = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0
rwa [aeval_def, ← eval_map] at ef0
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
⊢ ↑1 < ↑b
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
⊢ 1 < ↑b
rw [← Int.cast_one]
no goals
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : abs (x - ↑a / ↑b) < 1 / ↑b ^ (r + natDegree f)
⊢ ↑1 < ↑b
exact Int.cast_lt.mpr b1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ ↑b ^ natDegree f * abs (x - ↑a / ↑b) < 1 / A
refine' (lt_div_iff' hA).mpr _
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) ≤ ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
refine' lt_of_le_of_lt _ a1
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A ≤ ↑b ^ r
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) ≤ ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b))
gcongr
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ (1 + 1) ^ r ≤ ↑b ^ r
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ A ≤ ↑b ^ r
refine' hn.le.trans _
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ (1 + 1) ^ r ≤ ↑b ^ r
rw [one_add_one_eq_two]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h.hab
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 2 ≤ ↑b
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r
gcongr
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1.h.hab
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 2 ≤ ↑b
exact Int.cast_two.symm.le.trans (Int.cast_le.mpr (Int.add_one_le_iff.mpr b1))
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ natDegree f * abs (x - ↑a / ↑b)) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ natDegree f * abs (x - ↑a / ↑b)
lift b to ℕ using zero_le_one.trans b1.le
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
h : 1 ≤ (↑(Nat.pred b) + 1) ^ natDegree f * (abs (x - ↑a / (↑(Nat.pred b) + 1)) * A)
⊢ 1 / A ≤ ↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (x - ↑a / (↑b + 1)) * A)
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)
specialize h a b.pred
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
h : 1 ≤ ↑(Nat.succ (Nat.pred b)) ^ natDegree f * (abs (x - ↑a / ↑(Nat.succ (Nat.pred b))) * A)
⊢ 1 < b
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
h : 1 ≤ (↑(Nat.pred b) + 1) ^ natDegree f * (abs (x - ↑a / (↑(Nat.pred b) + 1)) * A)
⊢ 1 / A ≤ ↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)
rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
  div_le_iff hA] at h
no goals
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ natDegree f * abs (x - ↑a / ↑↑b)) < 1
b0 : 0 < ↑↑b
h : 1 ≤ ↑(Nat.succ (Nat.pred b)) ^ natDegree f * (abs (x - ↑a / ↑(Nat.succ (Nat.pred b))) * A)
⊢ 1 < b
exact Int.ofNat_lt.mp b1