awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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
⊢ (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty

Tactic:
have h : ((f.aroots ℂ).map c').toFinset.Nonempty := ⟨c' r, aux⟩
-- Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
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_1 :
  (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
h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty
⊢ c' r ≤
    if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h else 0

Tactic:
simpa only [h, ↓reduceDIte] using Finset.le_max' _ _ aux

Premises used: reduceDIte, Finset.le_max'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑{ num := a, den := b, den_nz := bN0, reduced := cop } : ℝ)
⊢ Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))

Tactic:
rw [Rat.cast_mk'] at h

Premises used: Rat.cast_mk'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
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
⊢ False

Tactic:
rcases h (b + 1) with ⟨p, q, q1, a0, a1⟩

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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)
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
have qR0 : (0 : ℝ) < q := Int.cast_pos.mpr (zero_lt_one.trans q1)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
⊢ Ne (α := ℝ) (↑b : ℝ) 0

Tactic:
have b0 : (b : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr bN0
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
⊢ 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)

Tactic:
have bq0 : (0 : ℝ) < b * q := mul_pos (Nat.cast_pos.mpr bN0.bot_lt) qR0
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
⊢ |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

Premises used: Iff.mpr, pow_pos, abs_div, LT.lt.ne', abs_pos, abs_of_pos, div_lt_div_iff₀, div_sub_div, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
a1₁ :
  |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
    HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑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

Premises used: Iff.mpr, pow_pos, abs_div, LT.lt.ne', abs_pos, abs_of_pos, div_lt_div_iff₀, div_sub_div, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
a1₁ :
  |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
    HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
qR0₁ : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ Ne (α := ℝ) (↑b : ℝ) 0

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

Premises used: Iff.mpr, pow_pos, abs_div, LT.lt.ne', abs_pos, abs_of_pos, div_lt_div_iff₀, div_sub_div, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
a1₁ :
  |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
    HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
qR0₁ : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0₁ : Ne (α := ℝ) (↑b : ℝ) 0
⊢ 0 < 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

Premises used: Iff.mpr, pow_pos, abs_div, LT.lt.ne', abs_pos, abs_of_pos, div_lt_div_iff₀, div_sub_div, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 :
  |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
    HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q

Tactic:
mod_cast a1

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, abs, congrArg, HSub.hSub, cast, Nat.cast, Int.cast_mul._simp_1, HPow.hPow, HAdd.hAdd, congr, LT.lt, Int.cast_lt._simp_1, Int.cast_pow._simp_1, Int.cast_abs._simp_1, OfNat.ofNat, Eq.symm, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 :
  |HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ)| * HPow.hPow (α := ℝ) (↑q : ℝ) (b + 1) <
    HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
qR0 : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0 : Ne (α := ℝ) (↑b : ℝ) 0
bq0 : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q

Tactic:
exact mod_cast a1
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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

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
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
⊢ ¬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

Premises used: Int.cast, sub_eq_zero, Ne, div_eq_div_iff, LT.lt.ne', mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
a0₁ : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
⊢ LT.lt (α := ℝ) 0 (↑q : ℝ)

Tactic:
rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0

Premises used: Int.cast, sub_eq_zero, Ne, div_eq_div_iff, LT.lt.ne', mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
a0₁ : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
qR0₁ : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ Ne (α := ℝ) (↑b : ℝ) 0

Tactic:
rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0

Premises used: Int.cast, sub_eq_zero, Ne, div_eq_div_iff, LT.lt.ne', mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
a0₁ : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
qR0₁ : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0₁ : Ne (α := ℝ) (↑b : ℝ) 0
⊢ 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)

Tactic:
rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0

Premises used: Int.cast, sub_eq_zero, Ne, div_eq_div_iff, LT.lt.ne', mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
a0₁ : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
qR0₁ : LT.lt (α := ℝ) 0 (↑q : ℝ)
b0₁ : Ne (α := ℝ) (↑b : ℝ) 0
bq0₁ : 0 < HMul.hMul (α := ℝ) (↑b : ℝ) (↑q : ℝ)
⊢ |a * q - (↑b : ℤ) * p| * q ^ (b + 1) < (↑b : ℤ) * q

Tactic:
rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0

Premises used: Int.cast, sub_eq_zero, Ne, div_eq_div_iff, LT.lt.ne', mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
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

Tactic:
mod_cast a0

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, Int.cast_zero, HSub.hSub, cast, Ne, Nat.cast, Int.cast_inj._simp_1, Int.cast_mul._simp_1, congr, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Eq, Not, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
p q : ℤ
q1 : 1 < q
a0 : ¬HMul.hMul (α := ℝ) (↑a : ℝ) (↑q : ℝ) - HMul.hMul (α := ℝ) (↑b : ℝ) (↑p : ℝ) = 0
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

Tactic:
exact mod_cast a0
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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

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
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
⊢ 0 ≤ q

Tactic:
(zero_lt_one.trans q1).le

Premises used: LT.lt.le, zero_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
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
⊢ False

Tactic:
lift q to ℕ using (zero_lt_one.trans q1).le

Premises used: LT.lt.le, zero_lt_one, LT.lt.trans
-- 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 : ℕ
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
⊢ 0 < |a * (↑q : ℤ) - (↑b : ℤ) * p|

Tactic:
have ap : 0 < |a * ↑q - ↑b * p| := abs_pos.mpr a0
-- 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 : ℕ
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|
⊢ 0 ≤ |a * (↑q : ℤ) - (↑b : ℤ) * p|

Tactic:
abs_nonneg (a * ↑q - ↑b * p)

Premises used: HMul.hMul, HSub.hSub, abs_nonneg
-- 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 : ℕ
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|
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
⊢ False

Tactic:
lift |a * ↑q - ↑b * p| to ℕ using abs_nonneg (a * ↑q - ↑b * p) with e he

Premises used: HMul.hMul, HSub.hSub, abs_nonneg
-- 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 : ℕ
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 : ℤ)
⊢ e * q ^ (b + 1) < b * q

Tactic:
norm_cast at a1 ap q1
-- 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 : ℕ
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
⊢ 0 < e

Tactic:
norm_cast at a1 ap q1
-- 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 : ℕ
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
⊢ 1 < q

Tactic:
norm_cast at a1 ap q1
-- 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:
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