-- Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
theorem exists_pos_real_of_irrational_root {α : ℝ} (ha : Irrational α) {f : ℤ[X]} (f0 : f ≠ 0)
    (fa : eval α (map (algebraMap ℤ ℝ) f) = 0) :
    ∃ A : ℝ, 0 < A ∧ ∀ a : ℤ, ∀ b : ℕ,
      (1 : ℝ) ≤ ((b : ℝ) + 1) ^ f.natDegree * (|α - a / (b + 1)| * A)

Proof state:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y (derivative fR)‖ ≤ |eval xm (derivative fR)|

Tactic:
exact hM h

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ |α - α| ≤ ζ

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ closedBall α ζ ∩ ↑fR.roots.toFinset

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

Result:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ fR.roots

Proof state:
case intro.intro.intro.intro.refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ dist α y * |eval xm (derivative fR)|

Tactic:
rw [mul_comm]

Result:
case intro.intro.intro.intro.refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ |eval xm (derivative fR)| * dist α y

Proof state:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * dist ((fun y => eval y fR) α) ((fun y => eval y fR) (↑z / (↑a + 1)))

Tactic:
show 1 ≤ (a + 1 : ℝ) ^ f.natDegree * |eval α fR - eval ((z : ℝ) / (a + 1)) fR|

Result:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval α fR - eval (↑z / (↑a + 1)) fR|

Proof state:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * |eval (↑z / (↑a + 1)) fR|

Tactic:
rw [show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast] at hq ⊢

Result:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ f.natDegree * |eval (↑z / ↑↑(a + 1)) fR|

Proof state:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ fR.roots

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

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ {α}

Tactic:
refine U.subset ?_

Result:
case intro.intro.intro.intro.refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ ↑z / ↑(↑a + 1) ∈ closedBall α ζ ∩ ↑fR.roots.toFinset

Proof state:
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

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

Result:
case intro.intro
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)