awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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
refine_2 : 1 / A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
    HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
refine (?_ : (b : ℝ) ^ f.natDegree * |x - a / b| < 1 / A).trans_le ?_

Premises used: LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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

Tactic:
(lt_div_iff₀' hA).mpr ?_

Premises used: Iff.mpr, lt_div_iff₀'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) < 1
⊢ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / A

Tactic:
refine (lt_div_iff₀' hA).mpr ?_

Premises used: Iff.mpr, lt_div_iff₀'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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

Tactic:
lt_of_le_of_lt ?_ a1

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 :
  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 : ℝ)|)
⊢ A * (HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|) < 1

Tactic:
refine lt_of_le_of_lt ?_ a1

Premises used: lt_of_le_of_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
⊢ 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:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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

Tactic:
hn.le.trans ?_

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : HAdd.hAdd (α := ℝ) 1 1 ^ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
⊢ A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r

Tactic:
refine hn.le.trans ?_

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 (α := ℝ) 2 r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r
⊢ HAdd.hAdd (α := ℝ) 1 1 ^ r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r

Tactic:
rw [one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : LE.le (α := ℝ) 2 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) 2 r ≤ HPow.hPow (α := ℝ) (↑b : ℝ) r

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 refine_1₁ refine_1₂ refine_1₃ : 2 ≤ b
⊢ LE.le (α := ℝ) 2 (↑b : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : ℝ)
⊢ 0 ≤ b

Tactic:
zero_le_one.trans b1.le

Premises used: LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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_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 : ℤ) : ℝ)|
⊢ 1 / A ≤ HPow.hPow (α := ℝ) (↑b : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
lift b to ℕ using zero_le_one.trans b1.le

Premises used: LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
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 : 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 ≤ HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1| * A)

Tactic:
specialize h a b.pred

Premises used: Nat.pred
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a : ℤ
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 : ℤ) : ℝ)
h : 1 ≤ HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1| * A)
rwa :
  ∀
    (h :
      1 ≤
        HPow.hPow (α := ℝ) (↑b.pred.succ : ℝ) f.natDegree * (|x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b.pred.succ : ℝ)| * A)),
    1 < b
⊢ 1 / A ≤ HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|

Tactic:
rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
      div_le_iff₀ hA] at h

Premises used: Nat.cast_succ, div_le_iff₀, Nat.succ_pred_eq_of_pos, mul_assoc, zero_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a : ℤ
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 : ℤ) : ℝ)
h : 1 ≤ HPow.hPow (α := ℝ) (↑b.pred.succ : ℝ) f.natDegree * (|x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b.pred.succ : ℝ)| * A)
⊢ 1 < b

Tactic:
Int.ofNat_lt.mp b1

Premises used: Int.ofNat_lt, Iff.mp
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a : ℤ
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 : ℤ) : ℝ)
h : 1 ≤ HPow.hPow (α := ℝ) (↑b.pred.succ : ℝ) f.natDegree * (|x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b.pred.succ : ℝ)| * A)
⊢ 1 < b

Tactic:
exact Int.ofNat_lt.mp b1

Premises used: Int.ofNat_lt, Iff.mp
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ 1 / m ^ i !

Tactic:
summable_one_div_pow_of_le hm Nat.self_le_factorial

Premises used: summable_one_div_pow_of_le, Nat.self_le_factorial
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ 1 / m ^ (n + (k + 1))!

Tactic:
(summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)

Premises used: Iff.mpr, summable_nat_add_iff, LiouvilleNumber.summable, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ 1 / m ^ (i + (k + 1))!

Tactic:
convert! (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)

Premises used: Iff.mpr, summable_nat_add_iff, LiouvilleNumber.summable, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
k x : ℕ
⊢ 0 ≤ 1 / m ^ (x + (k + 1))!

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
k : ℕ
⊢ 0 < 1 / m ^ (0 + (k + 1))!

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
n : ℕ
⊢ partialSum m (n + 1) = partialSum m n + 1 / m ^ (n + 1)!

Tactic:
sum_range_succ _ _

Premises used: LiouvilleNumber.partialSum, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℝ
hm : 1 < m
k : ℕ
⊢ partialSum m k + remainder m k = liouvilleNumber m

Tactic:
(LiouvilleNumber.summable hm).sum_add_tsum_nat_add _

Premises used: LiouvilleNumber.remainder, LiouvilleNumber.summable, liouvilleNumber, LiouvilleNumber.partialSum, Summable.sum_add_tsum_nat_add
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ Eq (α := ℝ) (∑' (i : ℕ), 1 / m ^ (i + (n + 1)!)) (∑' (i : ℕ), (1 / m) ^ i * (1 / m ^ (n + 1)!))

Tactic:
simp only [pow_add, one_div, mul_inv, inv_pow]

Premises used: mul_inv, pow_add, inv_pow, one_div
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ 0 ≤ 1 / m

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
rw rw₁ : (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)

Tactic:
rw [tsum_geometric_of_lt_one (by positivity) mi]

Premises used: tsum_geometric_of_lt_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
hbc : (1 - 1 / m)⁻¹ ≤ 2
⊢ (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ (1 - 1 / m)⁻¹ ≤ 2

Tactic:
sub_one_div_inv_le_two hm

Premises used: sub_one_div_inv_le_two
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ (1 - 1 / m)⁻¹ ≤ 2

Tactic:
exact sub_one_div_inv_le_two hm

Premises used: sub_one_div_inv_le_two
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
rw : m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !
hb : 0 < m ^ (n ! * (n + 1))
hd : 0 < m ^ (n ! * n)
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / (m ^ n !) ^ n

Tactic:
rw [← pow_mul, div_le_div_iff₀, one_mul, mul_add_one, pow_add, mul_comm 2]

Premises used: pow_add, pow_mul, div_le_div_iff₀, mul_comm, mul_add_one, OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
hbc : 2 ≤ m ^ n !
⊢ m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ n ! ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

Tactic:
exact hm.trans <| le_self_pow₀ (one_le_two.trans hm) <| by positivity

Premises used: le_self_pow₀, one_le_two, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * (n + 1))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 0 < m ^ (n ! * n)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
n : ℕ
m : ℝ
m2 : 2 ≤ m
⊢ remainder m n < 1 / (m ^ n !) ^ n

Tactic:
(remainder_lt' n <| one_lt_two.trans_le m2).trans_le (aux_calc _ m2)

Premises used: LiouvilleNumber.aux_calc, LT.lt.trans_le, one_lt_two, LiouvilleNumber.remainder_lt'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₃ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) 1 (↑(m ^ 0!) : ℝ)
rw₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 1 = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
rw₅ : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
rw₆ rw₇ : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)

Tactic:
rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]

Premises used: Finset.sum_singleton, Nat.factorial, pow_one, LiouvilleNumber.partialSum, Finset.range_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ 0!) : ℝ)

Tactic:
exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)
succ :
  ∀ (p_k : ℕ) (h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)),
    ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)

Tactic:
rcases h with ⟨p_k, h_k⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h : partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)

Tactic:
use p_k * m ^ ((k + 1)! - k !) + 1

Premises used: HSub.hSub, HAdd.hAdd, Nat.factorial, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
h₁ : (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
h₂ : Ne (α := ℝ) (↑(m ^ (k + 1)!) : ℝ) 0
h₃ : Ne (α := ℝ) (↑(m ^ k !) : ℝ) 0
h₄ : HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)

Tactic:
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]

Premises used: add_mul, div_eq_div_iff, div_add_div, LiouvilleNumber.partialSum_succ
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
⊢ (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)

Tactic:
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]

Premises used: add_mul, Nat.factorial_succ, pow_add, add_tsub_cancel_right, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
    p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ Ne (α := ℝ) (↑(m ^ (k + 1)!) : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ Ne (α := ℝ) (↑(m ^ k !) : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0

Tactic:
positivity