awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
y_1 : ℝ
hy : y_1 ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y ((derivative : (a : ℝ[X]) → ℝ[X]) fR)‖ ≤ |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|

Tactic:
exact hM h
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
refine_2 : |α - α| ≤ ζ
⊢ dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)| * dist α y

Tactic:
refine
      Convex.norm_image_sub_le_of_norm_deriv_le (fun _ _ => fR.differentiableAt)
        (fun y h => by rw [fR.deriv]; exact hM h) (convex_Icc _ _) hy (mem_Icc_iff_abs_le.mp ?_)

Premises used: Set.mem_Icc_iff_abs_le, convex_Icc, Convex.norm_image_sub_le_of_norm_deriv_le, Iff.mp, Polynomial.differentiableAt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ |α - α| ≤ ζ

Tactic:
@mem_closedBall_self ℝ _ α ζ (le_of_lt z0)

Premises used: Set.Mem, le_of_lt, Metric.closedBall, Metric.mem_closedBall_self
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ |α - α| ≤ ζ

Tactic:
exact @mem_closedBall_self ℝ _ α ζ (le_of_lt z0)

Premises used: le_of_lt, Metric.mem_closedBall_self
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : (↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ∈ closedBall α ζ
refine_3 : 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval α fR - eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|

Tactic:
rw [fa, zero_sub, abs_neg]

Premises used: abs_neg, zero_sub
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : (↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ∈ closedBall α ζ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a + 1 = a + 1
⊢ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 = (↑(↑(a + 1) : ℤ) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a + 1 = a + 1
⊢ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 = (↑(↑(a + 1) : ℤ) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : (↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ∈ closedBall α ζ
refine_3 :
  ∀ (hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ),
    1 ≤
      HPow.hPow (α := ℝ) (↑(↑(a + 1) : ℤ) : ℝ) f.natDegree *
        |eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) fR|
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|

Tactic:
rw [show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast] at hq ⊢
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
⊢ 1 ≤
    HPow.hPow (α := ℝ) (↑(↑(a + 1) : ℤ) : ℝ) f.natDegree * |eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) fR|

Tactic:
one_le_pow_mul_abs_eval_div (Int.natCast_succ_pos a) fun hy => ?_

Premises used: one_le_pow_mul_abs_eval_div, Int.natCast_succ_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
refine_3 : ∀ (hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0), False
⊢ 1 ≤
    HPow.hPow (α := ℝ) (↑(↑(a + 1) : ℤ) : ℝ) f.natDegree * |eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) fR|

Tactic:
refine one_le_pow_mul_abs_eval_div (Int.natCast_succ_pos a) fun hy => ?_

Premises used: one_le_pow_mul_abs_eval_div, Int.natCast_succ_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
⊢ False

Tactic:
ha.ne_rational z (a + 1) (mem_singleton_iff.mp ?_).symm

Premises used: Nat.cast, Irrational.ne_rational, Set.mem_singleton_iff, HAdd.hAdd, Iff.mp, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
refine_3 : Membership.mem (γ := Set ℝ) {α} (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ))
⊢ False

Tactic:
refine ha.ne_rational z (a + 1) (mem_singleton_iff.mp ?_).symm

Premises used: Nat.cast, Irrational.ne_rational, Set.mem_singleton_iff, HAdd.hAdd, Iff.mp, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
⊢ Membership.mem (γ := Set ℝ) {α} (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ))

Tactic:
U.subset ?_

Premises used: Eq.subset
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
refine_3 :
  HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ)
⊢ Membership.mem (γ := Set ℝ) {α} (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ))

Tactic:
refine U.subset ?_

Premises used: Eq.subset
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
⊢ HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ)

Tactic:
⟨hq, Finset.mem_coe.mp (Multiset.mem_toFinset.mpr ?_)⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.inter, And.intro, Iff.mp, Finset.mem_coe, Multiset.mem_toFinset
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
refine_3 : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ fR.roots
⊢ HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ)

Tactic:
refine ⟨hq, Finset.mem_coe.mp (Multiset.mem_toFinset.mpr ?_)⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
⊢ HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ fR.roots

Tactic:
(mem_roots fR0).mpr (IsRoot.def.mpr hy)

Premises used: Iff.mpr, Polynomial.IsRoot.def, Polynomial.mem_roots
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ (↑fR.roots.toFinset : Set ℝ)
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}
xm : ℝ
hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ
hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0
⊢ HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ fR.roots

Tactic:
exact (mem_roots fR0).mpr (IsRoot.def.mpr hy)

Premises used: Iff.mpr, Polynomial.IsRoot.def, Polynomial.mem_roots
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) f : ℝ) (0 : ℝ)
rwa rwa₁ rwa₂ rwa₃ : ∀ (ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0), eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

Tactic:
rwa [← eval_map_algebraMap] at ef0

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) f : ℝ) (0 : ℝ)
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

Tactic:
replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by
    rwa [← eval_map_algebraMap] at ef0
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)

Tactic:
exists_pos_real_of_irrational_root lx.irrational f0 ef0

Premises used: Liouville.irrational, Liouville.exists_pos_real_of_irrational_root
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
obtain :
  ∀ (A : ℝ) (hA : 0 < A)
    (h :
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)),
    False
⊢ 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

Premises used: Liouville.irrational, Liouville.exists_pos_real_of_irrational_root
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
rcases : ∀ (r : ℕ) (hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r), False
⊢ False

Tactic:
rcases pow_unbounded_of_one_lt A (lt_add_one 1) with ⟨r, hn⟩

Premises used: lt_add_one, OfNat.ofNat, pow_unbounded_of_one_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)

Tactic:
lx (r + f.natDegree)

Premises used: HAdd.hAdd, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
obtain :
  ∀ (a b : ℤ) (b1 : 1 < b)
    (a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)), False
⊢ 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)

Premises used: HAdd.hAdd, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
rw : LT.lt (α := ℝ) (↑1 : ℝ) (↑b : ℝ)
⊢ LT.lt (α := ℝ) 1 (↑b : ℝ)

Tactic:
rw [← Int.cast_one]

Premises used: Int.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
⊢ LT.lt (α := ℝ) (↑1 : ℝ) (↑b : ℝ)

Tactic:
Int.cast_lt.mpr b1

Premises used: Iff.mpr, Int.cast_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
⊢ LT.lt (α := ℝ) (↑1 : ℝ) (↑b : ℝ)

Tactic:
exact Int.cast_lt.mpr b1

Premises used: Iff.mpr, Int.cast_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
have b0 : (0 : ℝ) < b := zero_lt_one.trans (by rw [← Int.cast_one]; exact Int.cast_lt.mpr b1)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ False

Tactic:
lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) ?_

Premises used: Int.cast, lt_irrefl, HMul.hMul, abs, HSub.hSub, HDiv.hDiv, HPow.hPow, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
refine :
  HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
    HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ False

Tactic:
refine lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) ?_

Premises used: Int.cast, lt_irrefl, HMul.hMul, abs, HSub.hSub, HDiv.hDiv, HPow.hPow, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) r *
      (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) <
    1

Tactic:
rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1

Premises used: pow_pos, lt_div_iff₀', mul_assoc, pow_add
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)
b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
a1₁ :
  HPow.hPow (α := ℝ) (↑b : ℝ) r *
      (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) <
    1
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
rw [lt_div_iff₀' (pow_pos b0 _), pow_add, mul_assoc] at a1

Premises used: pow_pos, lt_div_iff₀', mul_assoc, pow_add
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a b : ℤ
b1 : 1 < b
a1 :
  HPow.hPow (α := ℝ) (↑b : ℝ) r *
      (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) <
    1
b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
    HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
(?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_

Premises used: LT.lt.trans_le