awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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)|
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have 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))
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 => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ζ
⊢ dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    dist α y * |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|
have refine_2 : dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
  |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)| * dist α y
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
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 α ζ
⊢ dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)| * dist α y
have hy₁ : y ∈ Icc (α - ζ) (α + ζ)
Tactic: rw [Real.closedBall_eq_Icc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 (α - ζ) (α + ζ)
⊢ Norm.norm (E := ℝ) (deriv (fun (x : ℝ) ↦ eval x fR) y) ≤ |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|
have rw : ‖eval y ((derivative : (a : ℝ[X]) → ℝ[X]) fR)‖ ≤ |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)|
Tactic: rw [fR.deriv]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 (α - ζ) (α + ζ)
⊢ dist (α := ℝ) ((fun (y : ℝ) ↦ eval y fR) α) ((fun (y : ℝ) ↦ eval y fR) y) ≤
    |eval xm ((derivative : (a : ℝ[X]) → ℝ[X]) fR)| * dist α y
have refine_2 : |α - α| ≤ ζ
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 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ζ
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval α fR - eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|
have refine_3 : 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|
Tactic: rw [fa, zero_sub, abs_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ζ
⊢ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 = (↑(↑(a + 1) : ℤ) : ℝ)
have norm_cast : a + 1 = a + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ζ
⊢ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 = (↑(↑(a + 1) : ℤ) : ℝ)
have norm_cast : a + 1 = a + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ζ
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree * |eval ((↑z : ℝ) / HAdd.hAdd (α := ℝ) (↑a : ℝ) 1) fR|
have refine_3 : ∀ (hq : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ) ∈ closedBall α ζ),
  1 ≤
    HPow.hPow (α := ℝ) (↑(↑(a + 1) : ℤ) : ℝ) f.natDegree * |eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) fR|
Tactic: rw [show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast] at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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|
have refine_3 : ∀ (hy : eval (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(↑(a + 1) : ℤ) : ℝ)) (map (algebraMap ℤ ℝ) f) = 0), False
Tactic: refine one_le_pow_mul_abs_eval_div (Int.natCast_succ_pos a) fun hy => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
have refine_3 : Membership.mem (γ := Set ℝ) {α} (HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ))
Tactic: refine ha.ne_rational z (a + 1) (mem_singleton_iff.mp ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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) : ℝ))
have refine_3 : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ closedBall α ζ ∩ (↑fR.roots.toFinset : Set ℝ)
Tactic: refine U.subset ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 ℝ)
have refine_3 : HDiv.hDiv (α := ℝ) (↑z : ℝ) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1) : ℝ) ∈ fR.roots
Tactic: refine ⟨hq, Finset.mem_coe.mp (Multiset.mem_toFinset.mpr ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) f : ℝ) (0 : ℝ)
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0
have rwa : ∀ (ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0), eval x (map (algebraMap ℤ ℝ) f) = 0
Tactic: rwa [← eval_map_algebraMap] at ef0
Cleared hypotheses: ef0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : Eq (α := ℝ) ((aeval x : (a : ℤ[X]) → ℝ) f : ℝ) (0 : ℝ)
⊢ False
have ef0₁ : eval x (map (algebraMap ℤ ℝ) f) = 0
Tactic: replace ef0 : (f.map (algebraMap ℤ ℝ)).eval x = 0 := by
    rwa [← eval_map_algebraMap] at ef0
Cleared hypotheses: ef0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
⊢ False
have obtain : ∀ (A : ℝ) (hA : 0 < A)
  (h :
    ∀ (a : ℤ) (b : ℕ),
      1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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)
⊢ False
have rcases : ∀ (r : ℕ) (hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r), False
Tactic: rcases pow_unbounded_of_one_lt A (lt_add_one 1) with ⟨r, hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
⊢ False
have obtain : ∀ (a b : ℤ) (b1 : 1 < b)
  (a1 : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (r + f.natDegree)), 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)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
have rw : LT.lt (α := ℝ) (↑1 : ℝ) (↑b : ℝ)
Tactic: rw [← Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
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)
⊢ False
have b0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
Tactic: have b0 : (0 : ℝ) < b := zero_lt_one.trans (by rw [← Int.cast_one]; exact Int.cast_lt.mpr b1)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
have refine : HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
  HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
Tactic: refine lt_irrefl ((b : ℝ) ^ f.natDegree * |x - ↑a / ↑b|) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
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 : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
    HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
have a1₁ : 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
Cleared hypotheses: a1, b0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)|
have refine_1 : HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / A
Tactic: refine (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
refine_1 : HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / A
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
    HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
have refine_2 : 1 / A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
Tactic: refine (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)| < 1 / A
have refine_1 : A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) < 1
Tactic: refine (lt_div_iff₀' hA).mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) < 1
have refine_1 : A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) ≤
  HPow.hPow (α := ℝ) (↑b : ℝ) r * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|)
Tactic: refine lt_of_le_of_lt ?_ a1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) ≤
    HPow.hPow (α := ℝ) (↑b : ℝ) r *
      (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|)
have refine_1 : A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
have refine_1 : HAdd.hAdd (α := ℝ) 1 1 ^ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
Tactic: refine hn.le.trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) 1 1 ^ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
have refine_1 : HPow.hPow (α := ℝ) 2 r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
Tactic: rw [one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 (α := ℝ) 2 r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
have refine_1 : LE.le (α := ℝ) 2 (↑b : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ LE.le (α := ℝ) 2 (↑b : ℝ)
have refine_1 : 2 ≤ b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 : ℝ)
⊢ 1 / A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
have refine_2 : ∀ (b : ℕ) (b1 : LT.lt (α := ℤ) 1 (↑b : ℤ))
  (a1 :
    HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) r *
        (HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|) <
      1)
  (b0 : LT.lt (α := ℝ) 0 (↑(↑b : ℤ) : ℝ)),
  1 / A ≤ HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|
Tactic: lift b to ℕ using zero_le_one.trans b1.le
Cleared hypotheses: b, b1, a1, b0