awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
apply :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    (HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))) ^
      k
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    HPow.hPow (β := ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
        (↑k : ℝ)⁻¹ *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))

Tactic:
apply le_of_pow_le_pow_left₀ hk <| mul_nonneg (rpow_nonneg (expr_pos hm notbdd).le _)
    (rpow_nonneg (apply_nonneg f ↑m) _)

Premises used: mul_nonneg, LT.lt.le, _private.0.Rat.AbsoluteValue.expr_pos, Real.rpow_nonneg, le_of_pow_le_pow_left₀, NonnegHomClass.apply_nonneg
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
nth_rewrite :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    HPow.hPow (β := ℝ)
      (HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
      (↑k : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    (HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))) ^
      k

Tactic:
nth_rewrite 2 [← rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
rw :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    HPow.hPow (β := ℝ)
      (HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
      (↑k : ℝ)

Tactic:
rw [mul_rpow (rpow_nonneg (expr_pos hm notbdd).le _) (rpow_nonneg (apply_nonneg f ↑m) _),
    ← rpow_mul (expr_pos hm notbdd).le, ← rpow_mul (apply_nonneg f ↑m),
    inv_mul_cancel₀ (mod_cast hk), rpow_one, mul_comm (logb ..)]

Premises used: Real.mul_rpow, LT.lt.le, Real.rpow_one, Real.logb, mul_comm, _private.0.Rat.AbsoluteValue.expr_pos, Real.rpow_nonneg, NonnegHomClass.apply_nonneg, Real.rpow_mul, inv_mul_cancel₀
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k = (f : (a : ℚ) → ℝ) (↑(n ^ k) : ℚ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
⊢ (f : (a : ℚ) → ℝ) (↑(n ^ k) : ℚ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑(n ^ k) : ℝ))

Tactic:
h_ineq1 hm (Nat.one_lt_pow hk hn)

Premises used: Nat.one_lt_pow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (HPow.hPow (α := ℝ) (↑n : ℝ) k)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))
rw₁ rw₂ :
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑(n ^ k) : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))

Tactic:
rw [Nat.cast_pow, logb_pow]

Premises used: Real.logb_pow, Nat.cast_pow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
h_ineq1 :
  ∀ {m n : ℕ} (hm : 1 < m) (hn : 1 < n),
    (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
k₁ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k = (f : (a : ℚ) → ℝ) (↑(n ^ k) : ℚ)
k₂ :
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑(n ^ k) : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))

Tactic:
calc
    (f n) ^ k = f ↑(n ^ k) := by simp
    _ ≤ (m * f m / (f m - 1)) * f m ^ logb m ↑(n ^ k) := h_ineq1 hm (Nat.one_lt_pow hk hn)
    _ = (m * f m / (f m - 1)) * f m ^ (k * logb m n) := by rw [Nat.cast_pow, logb_pow]

Premises used: Nat.one_lt_pow, HMul.hMul, HSub.hSub, HDiv.hDiv, Nat.cast, Real.logb, HPow.hPow, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
nth_rw :
  Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))
⊢ Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))

Tactic:
nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]

Premises used: Nat.cast, Real.logb, HPow.hPow, DFunLike.coe, one_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))

Tactic:
(tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _

Premises used: _private.0.tendsto_const_rpow_inv, Filter.Tendsto.mul_const, _private.0.Rat.AbsoluteValue.expr_pos
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))

Tactic:
exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _

Premises used: _private.0.tendsto_const_rpow_inv, Filter.Tendsto.mul_const, _private.0.Rat.AbsoluteValue.expr_pos
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))

Tactic:
have : Tendsto (fun k : ℕ ↦ (m * f m / (f m - 1)) ^ (k : ℝ)⁻¹ * f m ^ logb m n)
      atTop (𝓝 (f m ^ logb m n)) := by
    nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]
    exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
this :
  Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))

Tactic:
le_of_tendsto_of_tendsto (tendsto_const_nhds (x := f ↑n)) this <|
    eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (ne_zero_of_lt hb)⟩

Premises used: Iff.mpr, tendsto_const_nhds, ne_zero_of_lt, Exists.intro, _private.0.Rat.AbsoluteValue.param_upperbound, Filter.eventually_atTop, OfNat.ofNat, le_of_tendsto_of_tendsto
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
this :
  Tendsto
    (fun (k : ℕ) ↦
      HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)))
    atTop (𝓝 (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))

Tactic:
exact le_of_tendsto_of_tendsto (tendsto_const_nhds (x := f ↑n)) this <|
    eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (ne_zero_of_lt hb)⟩

Premises used: Iff.mpr, tendsto_const_nhds, ne_zero_of_lt, Exists.intro, _private.0.Rat.AbsoluteValue.param_upperbound, Filter.eventually_atTop, OfNat.ofNat, le_of_tendsto_of_tendsto
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
s t : ℝ
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hfn : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) t
rw : (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
⊢ t ≤ s

Tactic:
rw [← rpow_le_rpow_left_iff (x := n) (mod_cast hn), ← hfn]

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Real.rpow_le_rpow_left_iff, Nat.cast, LT.lt, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
s t : ℝ
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hfn : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) t
apply : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s

Tactic:
apply le_trans <| le_pow_log hm hn notbdd

Premises used: le_trans, Rat.AbsoluteValue.le_pow_log
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
s t : ℝ
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hfn : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) t
rw : HPow.hPow (α := ℝ) (↑m : ℝ) s ^ logb (↑m : ℝ) (↑n : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
rw₁ : HPow.hPow (α := ℝ) (↑m : ℝ) (s * logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
rw₂ : HPow.hPow (α := ℝ) (↑m : ℝ) (logb (↑m : ℝ) (↑n : ℝ) * s) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
rw₃ : HPow.hPow (α := ℝ) (↑m : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ^ s ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
rw₄ rw₅ : HPow.hPow (α := ℝ) (↑n : ℝ) s ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s

Tactic:
rw [hfm, ← rpow_mul (Nat.cast_nonneg m), mul_comm, rpow_mul (Nat.cast_nonneg m),
    rpow_logb (mod_cast zero_lt_of_lt hm) (mod_cast hm.ne') (mod_cast zero_lt_of_lt hn)]

Premises used: Nat.cast_nonneg, Real.rpow_logb, mul_comm, Real.rpow_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
s t : ℝ
hfm : (f : (a : ℚ) → ℝ) (↑m : ℚ) = HPow.hPow (α := ℝ) (↑m : ℝ) s
hfn : (f : (a : ℚ) → ℝ) (↑n : ℚ) = HPow.hPow (α := ℝ) (↑n : ℝ) t
⊢ s = t

Tactic:
le_antisymm (le_of_eq_pow hn hm notbdd hfn hfm) (le_of_eq_pow hm hn notbdd hfm hfn)

Premises used: le_antisymm, _private.0.Rat.AbsoluteValue.le_of_eq_pow
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
obtain : ∀ (m : ℕ) (hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)), f.IsEquiv real
⊢ f.IsEquiv real

Tactic:
obtain ⟨m, hm⟩ := Classical.exists_not_of_not_forall notbdd

Premises used: Classical.exists_not_of_not_forall
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
contrapose! : ∀ (hm : m ≤ 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ 1 < m

Tactic:
contrapose! hm
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : m ≤ 1
inl : ∀ (hm : LE.le (α := ℕ) 0 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) (1 : ℝ)
inr : ∀ (hm : LE.le (α := ℕ) 1 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) (1 : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hm : LE.le (α := ℕ) 0 1
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hm : LE.le (α := ℕ) 1 1
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ 1 < m

Tactic:
have oneltm : 1 < m := by
    contrapose! hm
    rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl <;> simp
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
rw : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (real : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ f.IsEquiv real

Tactic:
rw [← exists_nat_rpow_iff_isEquiv]

Premises used: Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
⊢ let s := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ));
  s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))

Tactic:
set s := logb m (f m) with hs

Premises used: Nat.cast, Real.logb, DFunLike.coe
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
⊢ ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (real : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
⟨s⁻¹,
    inv_pos.mpr (logb_pos (Nat.one_lt_cast.mpr oneltm) (one_lt_of_not_bounded notbdd oneltm)),
    fun n ↦ ?_⟩

Premises used: Iff.mpr, inv_pos, Inv.inv, And.intro, Nat.one_lt_cast, Exists.intro, Rat.AbsoluteValue.one_lt_of_not_bounded, Real.logb_pos
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
refine : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (real : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
refine ⟨s⁻¹,
    inv_pos.mpr (logb_pos (Nat.one_lt_cast.mpr oneltm) (one_lt_of_not_bounded notbdd oneltm)),
    fun n ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
inl : ∀ (h : n < 1), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
inr : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑1 : ℚ)
inr₁ : ∀ (h : 1 < n), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)

Tactic:
rcases lt_trichotomy n 1 with h | rfl | h

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
s : ℝ := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hs : s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
n : ℕ
h : n < 1
⊢ n = 0

Tactic:
lia