awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart (hypothesis)
Goal:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : (s : ℂ) → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' :
  eval 0 ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p)) =
    (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p).natDegree - p
r : ℂ
hr : r ∈ f.aroots ℂ
h :
  (aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) =
    HMul.hMul (α := ℂ) (β := ℂ) ((↑p ! : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this_1 :
  ((↑(eval 0 f ^ p + (↑p : ℤ) * eval 0 gp') : ℂ) * cexp r -
        HMul.hMul (α := ℂ) (β := ℂ) ((↑p : ℂ) : ℂ) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)) *
      (↑(p - 1)! : ℂ) =
    HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      (↑(p * (p - 1)!) : ℂ) * HSub.hSub (β := ℂ) ((↑(eval 0 gp') : ℂ) * cexp r) ((aeval r : (a : ℤ[X]) → ℂ) gp : ℂ)
this :
  HPow.hPow (α := ℂ) (↑(eval 0 f) : ℂ) p * cexp r * (↑(p - 1)! : ℂ) +
      HSub.hSub (β := ℂ) ((↑p ! : ℂ) * ((↑(eval 0 gp') : ℂ) * cexp r))
        ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
          ℂ) =
    HSub.hSub (β := ℂ) ((↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') : ℂ) * cexp r)
      ((aeval r : (a : ℤ[X]) → ℂ) ((sumIDeriv : (a : ℤ[X]) → ℤ[X]) (HPow.hPow (α := ℤ[X]) X (p - 1) * f ^ p) : ℤ[X]) :
        ℂ)
aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0
have h₁ : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty
Tactic: have h : ((f.aroots ℂ).map c').toFinset.Nonempty := ⟨c' r, aux⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑{ num := a, den := b, den_nz := bN0, reduced := cop } : ℝ)
⊢ False
have h₁ : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
Tactic: rw [Rat.cast_mk'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
⊢ False
have rcases : ∀ (p q : ℤ) (q1 : 1 < q) (a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ))
  (a1 :
    |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
      1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)),
  False
Tactic: rcases h (b + 1) with ⟨p, q, q1, a0, a1⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
a1 :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)
⊢ False
have qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
Tactic: have qR0 : (0 : ℝ) < q := Int.cast_pos.mpr (zero_lt_one.trans q1)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
a1 :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ False
have b0 : Ne (α := ℝ) (↑b : ℝ) 0
Tactic: have b0 : (b : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr bN0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
a1 :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
⊢ False
have bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
Tactic: have bq0 : (0 : ℝ) < b * q := mul_pos (Nat.cast_pos.mpr bN0.bot_lt) qR0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
a1 :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q
have a1₁ : |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
  HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
Tactic: rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _),
      abs_of_pos bq0, one_mul] at a1
Cleared hypotheses: a1, qR0, b0, bq0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
a1 :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ False
have a1₁ : |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q
Tactic: replace a1 : |a * q - b * p| * q ^ (b + 1) < b * q := by
    rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _),
      abs_of_pos bq0, one_mul] at a1
    exact mod_cast a1
Cleared hypotheses: a1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
a1 : |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q
⊢ a * q - (↑b : ℤ) * p ≠ 0
have a0₁ : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
Tactic: rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0
Cleared hypotheses: a0, qR0, b0, bq0, a1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑q : ℝ)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
a1 : |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q
⊢ False
have a0₁ : a * q - (↑b : ℤ) * p ≠ 0
Tactic: replace a0 : a * q - ↑b * p ≠ 0 := by
    rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0
    exact mod_cast a0
Cleared hypotheses: a0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
a1 : |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q
a0 : a * q - (↑b : ℤ) * p ≠ 0
⊢ False
have lift : ∀ (q : ℕ) (q1 : LT.lt (α := ℤ) 1 (↑q : ℤ)) (qR0 : LT.lt (α := ℝ) 0 (↑(↑q : ℤ) : ℝ))
  (bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑(↑q : ℤ) : ℝ))
  (a1 : |a * (↑q : ℤ) - (↑b : ℤ) * p| * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ))
  (a0 : a * (↑q : ℤ) - (↑b : ℤ) * p ≠ 0), False
Tactic: lift q to ℕ using (zero_lt_one.trans q1).le
Cleared hypotheses: q, q1, qR0, bq0, a1, a0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
q1 : LT.lt (α := ℤ) 1 (↑q : ℤ)
qR0 : LT.lt (α := ℝ) 0 (↑(↑q : ℤ) : ℝ)
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑(↑q : ℤ) : ℝ)
a1 : |a * (↑q : ℤ) - (↑b : ℤ) * p| * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ)
a0 : a * (↑q : ℤ) - (↑b : ℤ) * p ≠ 0
⊢ False
have ap : 0 < |a * (↑q : ℤ) - (↑b : ℤ) * p|
Tactic: have ap : 0 < |a * ↑q - ↑b * p| := abs_pos.mpr a0
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
q1 : LT.lt (α := ℤ) 1 (↑q : ℤ)
qR0 : LT.lt (α := ℝ) 0 (↑(↑q : ℤ) : ℝ)
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑(↑q : ℤ) : ℝ)
a1 : |a * (↑q : ℤ) - (↑b : ℤ) * p| * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ)
a0 : a * (↑q : ℤ) - (↑b : ℤ) * p ≠ 0
ap : 0 < |a * (↑q : ℤ) - (↑b : ℤ) * p|
⊢ False
have lift : ∀ (e : ℕ) (he : (↑e : ℤ) = |a * (↑q : ℤ) - (↑b : ℤ) * p|)
  (a1 : (↑e : ℤ) * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ))
  (ap : LT.lt (α := ℤ) 0 (↑e : ℤ)), False
Tactic: lift |a * ↑q - ↑b * p| to ℕ using abs_nonneg (a * ↑q - ↑b * p) with e he
Cleared hypotheses: a1, ap
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
q1 : LT.lt (α := ℤ) 1 (↑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 : ℤ) * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ)
ap : LT.lt (α := ℤ) 0 (↑e : ℤ)
⊢ False
have a1₁ : e * q ^ (b + 1) < b * q
Tactic: norm_cast at a1 ap q1
Cleared hypotheses: q1, a1, ap
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
q1 : LT.lt (α := ℤ) 1 (↑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 : ℤ) * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ)
ap : LT.lt (α := ℤ) 0 (↑e : ℤ)
a1₁ : e * q ^ (b + 1) < b * q
⊢ False
have ap₁ : 0 < e
Tactic: norm_cast at a1 ap q1
Cleared hypotheses: q1, a1, ap
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p : ℤ
b0 : Ne (α := ℝ) (↑b : ℝ) 0
q : ℕ
q1 : LT.lt (α := ℤ) 1 (↑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 : ℤ) * HPow.hPow (α := ℤ) (↑q : ℤ) (b + 1) < HMul.hMul (α := ℤ) (↑b : ℤ) (↑q : ℤ)
ap : LT.lt (α := ℤ) 0 (↑e : ℤ)
a1₁ : e * q ^ (b + 1) < b * q
ap₁ : 0 < e
⊢ False
have q1₁ : 1 < q
Tactic: norm_cast at a1 ap q1
Cleared hypotheses: q1, a1, ap
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
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))
⊢ ∃ (A : ℝ), 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
have me0 : 0 < max (1 / ε) M
Tactic: have me0 : 0 < max (1 / ε) M := lt_max_iff.mpr (Or.inl (one_div_pos.mpr e0))
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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)
have refine : ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
Tactic: refine ⟨max (1 / ε) M, me0, fun z a => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
have pos : ∀ (dm1 : 1 ≤ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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)
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)
have neg : ∀ (dm1 : ¬1 ≤ 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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ε
have refine : dist α (j z a) ≤ 1 / max (1 / ε) M
Tactic: refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
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)
have this : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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)
have neg : d a * dist (f α) (f (j z a)) ≤ d a * (dist α (j z a) * max (1 / ε) M)
Tactic: refine (L this).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α ε
⊢ d a * dist (f α) (f (j z a)) ≤ d a * (dist α (j z a) * max (1 / ε) M)
have neg : 0 ≤ d a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
⊢ d a * dist (f α) (f (j z a)) ≤ d a * (dist α (j z a) * max (1 / ε) M)
have neg₁ : dist (f α) (f (j z a)) ≤ dist α (j z a) * max (1 / ε) M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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
have neg : dist α (j z a) * M ≤ dist α (j z a) * max (1 / ε) M
Tactic: refine (B this).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
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 α (j z a) * M ≤ dist α (j z a) * max (1 / ε) M
have neg : M ≤ max (1 / ε) M
Tactic: gcongr
-- 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
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have fR0 : 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)
-- 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
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have ar : α ∈ (↑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)))
-- 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 ℝ)
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have 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)
Tactic: obtain ⟨ζ, z0, U⟩ : ∃ ζ > 0, closedBall α ζ ∩ fR.roots.toFinset = {α} :=
    @exists_closedBall_inter_eq_singleton_of_discrete _ _ _ (toFinite _).isDiscrete _ ar
-- 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 ℝ) = {α}
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have 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)
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
-- 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
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have refine_1 : ∀ (a : ℕ), 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree
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
refine_1 : ∀ (a : ℕ), 1 ≤ HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ f.natDegree
⊢ ∃ (A : ℝ),
    0 < A ∧
      ∀ (a : ℤ) (b : ℕ),
        1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|α - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
have 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)|
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 => ?_