α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fa : eval α (map (algebraMap ℤ ℝ) f) = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
set fR : ℝ[X] := map (algebraMap ℤ ℝ) f
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
obtain fR0 : fR ≠ 0 := fun fR0 =>
  (map_injective (algebraMap ℤ ℝ) fun _ _ A => Int.cast_inj.mp A).ne f0
    (fR0.trans (Polynomial.map_zero _).symm)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
have ar : α ∈ (fR.roots.toFinset : Set ℝ) :=
  Finset.mem_coe.mpr (Multiset.mem_toFinset.mpr ((mem_roots fR0).mpr (IsRoot.def.mpr fa)))
case intro.intro
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
obtain ⟨ζ, z0, U⟩ : ∃ ζ > 0, closedBall α ζ ∩ fR.roots.toFinset = {α} :=
  @exists_closedBall_inter_eq_singleton_of_discrete _ _ _ discrete_of_t1_of_finite _ ar
case intro.intro.intro.intro.refine'_1
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
⊢ ∀ (a : ℕ), 1 ≤ (↑a + 1) ^ natDegree f

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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ dist α y * abs (eval xm (↑derivative fR))

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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * dist ((fun y => eval y fR) α) ((fun y => eval y fR) (↑z / (↑a + 1)))
case intro.intro.intro.intro
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ natDegree f * (abs (α - ↑a / (↑b + 1)) * A)
refine'
  @exists_one_le_pow_mul_dist ℤ ℕ ℝ _ _ _ (fun y => fR.eval y) α ζ (|fR.derivative.eval xm|) _ z0
    (fun y hy => _) fun z a hq => _
no goals
case intro.intro.intro.intro.refine'_1
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
⊢ ∀ (a : ℕ), 1 ≤ (↑a + 1) ^ natDegree f
exact fun a => one_le_pow_of_one_le ((le_add_iff_nonneg_left 1).mpr a.cast_nonneg) _
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ abs (eval xm (↑derivative fR)) * dist α y
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ dist α y * abs (eval xm (↑derivative fR))
rw [mul_comm]
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ abs (eval xm (↑derivative fR)) * dist α y
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ abs (eval xm (↑derivative fR)) * dist α y
rw [Real.closedBall_eq_Icc] at hy
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ abs (α - α) ≤ ζ
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ abs (eval xm (↑derivative fR)) * dist α y
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 _)
no goals
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ Icc (α - ζ) (α + ζ)
⊢ abs (α - α) ≤ ζ
exact @mem_closedBall_self ℝ _ α ζ (le_of_lt z0)
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y (↑derivative fR)‖ ≤ abs (eval xm (↑derivative fR))
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖deriv (fun x => eval x fR) y‖ ≤ abs (eval xm (↑derivative fR))
rw [fR.deriv]
no goals
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
y✝ : ℝ
hy : y✝ ∈ Icc (α - ζ) (α + ζ)
y : ℝ
h : y ∈ Icc (α - ζ) (α + ζ)
⊢ ‖eval y (↑derivative fR)‖ ≤ abs (eval xm (↑derivative fR))
exact hM h
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * abs (eval α fR - eval (↑z / (↑a + 1)) fR)
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * dist ((fun y => eval y fR) α) ((fun y => eval y fR) (↑z / (↑a + 1)))
show 1 ≤ (a + 1 : ℝ) ^ f.natDegree * |eval α fR - eval ((z : ℝ) / (a + 1)) fR|
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * abs (eval (↑z / (↑a + 1)) fR)
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * abs (eval α fR - eval (↑z / (↑a + 1)) fR)
rw [fa, zero_sub, abs_neg]
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ natDegree f * abs (eval (↑z / ↑↑(a + 1)) fR)
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ natDegree f * abs (eval (↑z / (↑a + 1)) fR)
rw [show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast] at hq ⊢
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ False
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ 1 ≤ ↑↑(a + 1) ^ natDegree f * abs (eval (↑z / ↑↑(a + 1)) fR)
refine' one_le_pow_mul_abs_eval_div (Int.coe_nat_succ_pos a) fun hy => _
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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) ∈ {α}
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
hy : eval (↑z / ↑↑(a + 1)) (map (algebraMap ℤ ℝ) f) = 0
⊢ False
refine' (irrational_iff_ne_rational α).mp ha z (a + 1) (mem_singleton_iff.mp _).symm
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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 α ζ ∩ ↑(Multiset.toFinset (roots fR))
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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) ∈ {α}
refine' U.subset _
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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) ∈ roots fR
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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 α ζ ∩ ↑(Multiset.toFinset (roots fR))
refine' ⟨hq, Finset.mem_coe.mp (Multiset.mem_toFinset.mpr _)⟩
no goals
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 : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (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) ∈ roots fR
exact (mem_roots fR0).mpr (IsRoot.def.mpr hy)
no goals
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑(Multiset.toFinset (roots fR))
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑(Multiset.toFinset (roots fR)) = {α}
xm : ℝ
hM : IsMaxOn (fun x => abs (eval x (↑derivative fR))) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / ↑↑(a + 1) ∈ closedBall α ζ
⊢ ↑a + 1 = ↑↑(a + 1)
norm_cast