awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
qR0 : LT.lt (α := ℝ) 0 (↑(↑q : ℤ) : ℝ)
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑(↑q : ℤ) : ℝ)
a0 : a * (↑q : ℤ) - (↑b : ℤ) * p ≠ 0
e : ℕ
he : (↑e : ℤ) = |a * (↑q : ℤ) - (↑b : ℤ) * p|
a1 : e * q ^ (b + 1) < b * q
ap : 0 < e
q1 : 1 < q
⊢ False

Tactic:
exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ ap q1).le

Premises used: not_le, Iff.mpr, LT.lt.le, Nat.mul_lt_mul_pow_succ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
⊢ 0 < max (1 / ε) M

Tactic:
have me0 : 0 < max (1 / ε) M := lt_max_iff.mpr (Or.inl (one_div_pos.mpr e0))
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
⊢ ∃ (A : ℝ), 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)

Tactic:
⟨max (1 / ε) M, me0, fun z a => ?_⟩

Premises used: HDiv.hDiv, Max.max, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
refine : ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
⊢ ∃ (A : ℝ), 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)

Tactic:
refine ⟨max (1 / ε) M, me0, fun z a => ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
pos : ∀ (dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M), 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
neg : ∀ (dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M), 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
by_cases dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M

Premises used: HDiv.hDiv, Max.max, Dist.dist, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
one_le_mul_of_one_le_of_one_le (d0 a) dm1

Premises used: one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : 1 ≤ dist α (j z a) * max (1 / ε) M
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
exact one_le_mul_of_one_le_of_one_le (d0 a) dm1

Premises used: one_le_mul_of_one_le_of_one_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ j z a ∈ closedBall α ε

Tactic:
mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))

Premises used: Iff.mpr, Set.Mem, setOf, Metric.mem_closedBall', one_div_le, Iff.mp, Metric.closedBall, le_max_left, le_trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
refine : dist α (j z a) ≤ 1 / max (1 / ε) M
⊢ j z a ∈ closedBall α ε

Tactic:
refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))

Premises used: Iff.mpr, Metric.mem_closedBall', one_div_le, Iff.mp, le_max_left, le_trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ dist α (j z a) ≤ 1 / max (1 / ε) M

Tactic:
(le_div_iff₀ me0).mpr (not_le.mp dm1).le

Premises used: not_le, Iff.mpr, LT.lt.le, Iff.mp, le_div_iff₀
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ dist α (j z a) ≤ 1 / max (1 / ε) M

Tactic:
exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le

Premises used: not_le, Iff.mpr, LT.lt.le, Iff.mp, le_div_iff₀
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ j z a ∈ closedBall α ε

Tactic:
have : j z a ∈ closedBall α ε := by
      refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
      exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
(L this).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
neg : d a * dist (f α) (f (j z a)) ≤ d a * (dist α (j z a) * max (1 / ε) M)
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
refine (L this).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
neg : 0 ≤ d a
neg₁ : dist (f α) (f (j z a)) ≤ dist α (j z a) * max (1 / ε) M
⊢ d a * dist (f α) (f (j z a)) ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ 0 ≤ d a

Tactic:
zero_le_one.trans (d0 a)

Premises used: zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ 0 ≤ d a

Tactic:
exact zero_le_one.trans (d0 a)

Premises used: zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ dist (f α) (f (j z a)) ≤ dist α (j z a) * max (1 / ε) M

Tactic:
(B this).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
neg : dist α (j z a) * M ≤ dist α (j z a) * max (1 / ε) M
⊢ dist (f α) (f (j z a)) ≤ dist α (j z a) * max (1 / ε) M

Tactic:
refine (B this).trans ?_

Premises used: LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
neg : M ≤ max (1 / ε) M
⊢ dist α (j z a) * M ≤ dist α (j z a) * max (1 / ε) M

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
Z : Type u_1
N : Type u_2
R : Type u_3
inst : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
this : j z a ∈ closedBall α ε
⊢ M ≤ max (1 / ε) M

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fa : eval α (map (algebraMap ℤ ℝ) f) = 0
⊢ let fR := map (algebraMap ℤ ℝ) f;
  eval α fR = 0

Tactic:
set fR : ℝ[X] := map (algebraMap ℤ ℝ) f

Premises used: Real, Algebra.algebraMap, Int, Polynomial.map
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ fR ≠ 0

Tactic:
fun fR0 =>
    (map_injective (algebraMap ℤ ℝ) fun _ _ A => Int.cast_inj.mp A).ne f0
      (fR0.trans (Polynomial.map_zero _).symm)

Premises used: Real, Int.cast_inj, Algebra.algebraMap, Function.Injective.ne, Polynomial.map_injective, Int, Polynomial.map_zero, Iff.mp, Eq.symm, Not, Eq.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ fR ≠ 0

Tactic:
obtain fR0 : fR ≠ 0 := fun fR0 =>
    (map_injective (algebraMap ℤ ℝ) fun _ _ A => Int.cast_inj.mp A).ne f0
      (fR0.trans (Polynomial.map_zero _).symm)

Premises used: Real, Int.cast_inj, Algebra.algebraMap, Function.Injective.ne, Polynomial.map_injective, Int, Iff.mp
-- 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
⊢ α ∈ (↑fR.roots.toFinset : Set ℝ)

Tactic:
have ar : α ∈ (fR.roots.toFinset : Set ℝ) :=
    Finset.mem_coe.mpr (Multiset.mem_toFinset.mpr ((mem_roots fR0).mpr (IsRoot.def.mpr fa)))
-- 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 ℝ)
⊢ ∃ ζ > 0, closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}

Tactic:
@exists_closedBall_inter_eq_singleton_of_discrete _ _ _ (toFinite _).isDiscrete _ ar

Premises used: Set.Finite.isDiscrete, Set.toFinite, Metric.exists_closedBall_inter_eq_singleton_of_discrete
-- 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 ℝ)
obtain :
  ∀ (ζ : ℝ) (z0 : ζ > 0) (U : closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ) = {α}),
    ∃ (A : ℝ),
      0 < A ∧
        ∀ (a : ℤ) (b : ℕ),
          1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)

Tactic:
obtain ⟨ζ, z0, U⟩ : ∃ ζ > 0, closedBall α ζ ∩ fR.roots.toFinset = {α} :=
    @exists_closedBall_inter_eq_singleton_of_discrete _ _ _ (toFinite _).isDiscrete _ ar

Premises used: Multiset.toFinset, Polynomial.roots, Set.Finite.isDiscrete, Set.toFinite, Metric.exists_closedBall_inter_eq_singleton_of_discrete
-- 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 ∈ Icc (α - ζ) (α + ζ),
    IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm

Tactic:
IsCompact.exists_isMaxOn isCompact_Icc
      ⟨α, (sub_lt_self α z0).le, (lt_add_of_pos_right α z0).le⟩
      (continuous_abs.comp fR.derivative.continuous_aeval).continuousOn

Premises used: Polynomial.derivative, Polynomial.continuous_aeval, lt_add_of_pos_right, Continuous.continuousOn, Set.Mem, sub_lt_self, Continuous.comp, LT.lt.le, CompactIccSpace.isCompact_Icc, And.intro, Exists.intro, continuous_abs, DFunLike.coe, IsCompact.exists_isMaxOn
-- 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 ℝ) = {α}
obtain :
  ∀ (xm : ℝ)
    (hM : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ |eval x ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|) (Icc (α - ζ) (α + ζ)) xm),
    ∃ (A : ℝ),
      0 < A ∧
        ∀ (a : ℤ) (b : ℕ),
          1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)

Tactic:
obtain ⟨xm, -, hM⟩ : ∃ xm : ℝ, xm ∈ Icc (α - ζ) (α + ζ) ∧
      IsMaxOn (|fR.derivative.eval ·|) (Icc (α - ζ) (α + ζ)) xm :=
    IsCompact.exists_isMaxOn isCompact_Icc
      ⟨α, (sub_lt_self α z0).le, (lt_add_of_pos_right α z0).le⟩
      (continuous_abs.comp fR.derivative.continuous_aeval).continuousOn

Premises used: Polynomial.derivative, Polynomial.continuous_aeval, lt_add_of_pos_right, Continuous.continuousOn, sub_lt_self, Continuous.comp, HSub.hSub, LT.lt.le, CompactIccSpace.isCompact_Icc, Set.Icc, HAdd.hAdd, And.intro, Exists.intro, continuous_abs, DFunLike.coe, IsCompact.exists_isMaxOn
-- 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
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)

Tactic:
@exists_one_le_pow_mul_dist ℤ ℕ ℝ _ _ _ (fun y => fR.eval y) α ζ |fR.derivative.eval xm| ?_ z0
      (fun y hy => ?_) fun z a hq => ?_

Premises used: Liouville.exists_one_le_pow_mul_dist
-- 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
refine_1 : ∀ (a : ℕ), 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree
refine_2 :
  ∀ (y : ℝ) (hy : y ∈ closedBall α ζ),
    dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
      dist α y * |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|
refine_3 :
  ∀ (z : ℤ) (a : ℕ) (hq : (↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ∈ closedBall α ζ),
    1 ≤
      HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree *
        dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α)
          ((fun (y : ℝ) ↦ eval y fR) ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1))
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)

Tactic:
refine
    @exists_one_le_pow_mul_dist ℤ ℕ ℝ _ _ _ (fun y => fR.eval y) α ζ |fR.derivative.eval xm| ?_ z0
      (fun y hy => ?_) fun z a hq => ?_

Premises used: Liouville.exists_one_le_pow_mul_dist
-- 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
⊢ ∀ (a : ℕ), 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree

Tactic:
fun a => one_le_pow₀ ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg)

Premises used: Iff.mpr, one_le_pow₀, OfNat.ofNat, le_add_iff_nonneg_left
-- 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
⊢ ∀ (a : ℕ), 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree

Tactic:
exact fun a => one_le_pow₀ ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg)

Premises used: Iff.mpr, one_le_pow₀, OfNat.ofNat, le_add_iff_nonneg_left
-- 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 ∈ closedBall α ζ
refine_2 :
  dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)| * dist α y
⊢ dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    dist α y * |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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 ∈ closedBall α ζ
⊢ y ∈ Icc (α - ζ) (α + ζ)

Tactic:
rw [Real.closedBall_eq_Icc] at hy

Premises used: Real.closedBall_eq_Icc
-- 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 (α - ζ) (α + ζ)
rw : ‖eval y ((derivative : (a : ℝ[X]) → ℝ[X]) fR)‖ ≤ |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|
⊢ Norm.norm (E := ℝ) (deriv (fun (x : ℝ) ↦ eval x fR) y) ≤ |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|

Tactic:
rw [fR.deriv]

Premises used: Polynomial.deriv
-- 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:
hM h

Premises used: Set.Mem