-- Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
theorem transcendental {x : ℝ} (lx : Liouville x) : Transcendental ℤ x

Proof state:
x : ℝ
lx : Liouville x
⊢ Transcendental ℤ x

Tactic:
rintro ⟨f : ℤ[X], f0, ef0⟩

Result:
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : (aeval x) f = 0
⊢ False

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
lift b to ℕ using zero_le_one.trans b1.le

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a : ℤ
b : ℕ
b1 : 1 < ↑b
a1 : ↑↑b ^ r * (↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
⊢ 1 / A ≤ ↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ 1 < ↑b

Tactic:
rw [← Int.cast_one]

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ ↑1 < ↑b

Proof state:
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ False

Tactic:
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

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
⊢ False

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
⊢ False

Tactic:
obtain ⟨a, b, b1, -, a1⟩ : ∃ a b : ℤ, 1 < b ∧ x ≠ a / b ∧
    |x - a / b| < 1 / (b : ℝ) ^ (r + f.natDegree) :=
  lx (r + f.natDegree)

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ False

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ f.natDegree * |x - ↑a / ↑b|) ≤ ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|)

Tactic:
gcongr

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A ≤ ↑b ^ r

Proof state:
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 ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
h : 1 ≤ (↑b.pred + 1) ^ f.natDegree * (|x - ↑a / (↑b.pred + 1)| * A)
⊢ 1 / A ≤ ↑↑b ^ f.natDegree * |x - ↑a / ↑↑b|

Tactic:
rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
  div_le_iff₀ hA] at h

Result:
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 ^ f.natDegree * |x - ↑a / ↑↑b|) < 1
b0 : 0 < ↑↑b
h : 1 ≤ ↑b.pred.succ ^ f.natDegree * (|x - ↑a / ↑b.pred.succ| * A)
⊢ 1 < b

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ^ r ≤ ↑b ^ r

Tactic:
gcongr

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ≤ ↑b

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 2 ≤ ↑b

Tactic:
exact Int.cast_two.symm.le.trans (Int.cast_le.mpr (Int.add_one_le_iff.mpr b1))

Result:
no goals

Proof state:
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : (aeval x) f = 0
⊢ False

Tactic:
replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by
  rwa [aeval_def, ← eval_map] at ef0

Result:
case intro.intro
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ False

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A ≤ ↑b ^ r

Tactic:
refine hn.le.trans ?_

Result:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ (1 + 1) ^ r ≤ ↑b ^ r

Proof state:
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) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
⊢ ↑1 < ↑b

Tactic:
exact Int.cast_lt.mpr b1

Result:
no goals