awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)|
have ha : LT.lt (α := ℝ) 0 |(↑r : ℝ)|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
have refine_2 : C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
  HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
Tactic: calc _ < C / ↑n ^ p * |↑r| := by gcongr
      _ = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
have refine_2 : |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)
Tactic: rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 : |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
have refine_2₁ : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
Tactic: rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 : |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)
refine_2₁ : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
have refine_2₂ : LE.le (α := ℝ) 0 (↑r.den : ℝ)
Tactic: rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 : |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)
refine_2₁ : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
refine_2₂ : LE.le (α := ℝ) 0 (↑r.den : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
have refine_2₃ : LE.le (α := ℝ) 0 (↑n : ℝ)
Tactic: rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
hr : r ≠ 0
⊢ LiouvilleWith p ((↑r : ℝ) * x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x * (↑r : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_rat_iff hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
hr : r ≠ 0
rw : LiouvilleWith p (x * (↑r : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑r : ℝ) * x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_rat_iff hr]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (x * (↑m : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x * (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast, mul_rat_iff (Int.cast_ne_zero.2 hm)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
hm : m ≠ 0
rw : LiouvilleWith p (x * (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x * (↑m : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast, mul_rat_iff (Int.cast_ne_zero.2 hm)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p ((↑m : ℝ) * x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x * (↑m : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_int_iff hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
hm : m ≠ 0
rw : LiouvilleWith p (x * (↑m : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑m : ℝ) * x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_int_iff hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (x * (↑n : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x * (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast, mul_rat_iff (Nat.cast_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
hn : n ≠ 0
rw : LiouvilleWith p (x * (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x * (↑n : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast, mul_rat_iff (Nat.cast_ne_zero.2 hn)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p ((↑n : ℝ) * x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x * (↑n : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_nat_iff hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
hn : n ≠ 0
rw : LiouvilleWith p (x * (↑n : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑n : ℝ) * x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [mul_comm, mul_nat_iff hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p ((↑n : ℝ) * x)
have rw : LiouvilleWith p (x * (↑n : ℝ))
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + (↑r : ℝ))
have rcases : ∀ (C : ℝ) (_hC₀ : 0 < C)
  (hC :
    ∃ᶠ (n : ℕ) in atTop,
      1 ≤ n ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p),
  LiouvilleWith p (x + (↑r : ℝ))
Tactic: rcases h.exists_pos with ⟨C, _hC₀, hC⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ LiouvilleWith p (x + (↑r : ℝ))
have refine : ∀ (x_1 : ℕ),
  (1 ≤ x_1 ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < C / HPow.hPow (α := ℝ) (↑x_1 : ℝ) p) →
    ∃ (m : ℤ),
      x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id x_1) : ℝ) ∧
        |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id x_1) : ℝ)| <
          HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id x_1) : ℝ) p
Tactic: refine ⟨r.den ^ p * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
have rw : HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
Tactic: rw [smul_eq_mul, id]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
have nth_rewrite : HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑(HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ)) : ℝ)
Tactic: nth_rewrite 4 [← Rat.num_div_den r]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑(HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ)) : ℝ)
have push_cast : (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
    HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
      HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
have rw : HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) +
    HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
Tactic: rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
rw :
  HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) +
      HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
⊢ (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
      HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
have rw₁ : HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) +
    HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
Tactic: rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
rw :
  HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) +
      HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
rw₁ :
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) +
      HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
⊢ (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
      HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
have rw₂ : HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
Tactic: rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (m : ℤ),
    x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ) ∧
      |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ)| <
        HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have this : HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
Tactic: have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
    rw [smul_eq_mul, id]
    nth_rewrite 4 [← Rat.num_div_den r]
    push_cast
    rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ ∃ (m : ℤ),
    x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ) ∧
      |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ)| <
        HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have refine : x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) ∧
  |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
Tactic: refine ⟨r.den * m + r.num * n, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) ∧
    |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have rw : x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ) ∧
  |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
Tactic: rw [this, add_sub_add_right_eq_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ) ∧
    |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have refine : C / HPow.hPow (α := ℝ) (↑n : ℝ) p = HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
Tactic: refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
C : ℝ
_hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p = HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have this₁ : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
Tactic: have : (r.den ^ p : ℝ) ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p ((↑r : ℝ) + x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + (↑r : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
rw : LiouvilleWith p (x + (↑r : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑r : ℝ) + x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x + (↑m : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast m, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
rw : LiouvilleWith p (x + (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x + (↑m : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast m, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p ((↑m : ℝ) + x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + (↑m : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_int_iff]