awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) ≤
    HPow.hPow (β := ℝ)
        (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
          HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
        (↑k : ℝ)⁻¹ *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have 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
Tactic: apply le_of_pow_le_pow_left₀ hk <| mul_nonneg (rpow_nonneg (expr_pos hm notbdd).le _)
    (rpow_nonneg (apply_nonneg f ↑m) _)
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 ≤
    (HPow.hPow (β := ℝ)
          (HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
            HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
          (↑k : ℝ)⁻¹ *
        HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))) ^
      k
have 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 : ℝ)
Tactic: nth_rewrite 2 [← rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 ≤
    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 : ℝ)
have 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 : ℝ))
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 ..)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ))
⊢ 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 : ℝ))
have 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 : ℝ))
Tactic: rw [Nat.cast_pow, logb_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ))
⊢ 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 : ℝ))
have 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 : ℝ))
Tactic: rw [Nat.cast_pow, logb_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ((↑k : ℝ) * logb (↑m : ℝ) (↑n : ℝ))
have k₁ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) k = (f : (a : ℚ) → ℝ) (↑(n ^ k) : ℚ)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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) : ℚ)
⊢ 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 : ℝ))
have 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 : ℝ))
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ))))
have 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 : ℝ))))
Tactic: nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have 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 : ℝ))))
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 _
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ t ≤ s
have rw : (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
Tactic: rw [← rpow_le_rpow_left_iff (x := n) (mod_cast hn), ← hfn]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have apply : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
Tactic: apply le_trans <| le_pow_log hm hn notbdd
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have rw : HPow.hPow (α := ℝ) (↑m : ℝ) s ^ 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have rw₁ : HPow.hPow (α := ℝ) (↑m : ℝ) (s * 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have rw₂ : HPow.hPow (α := ℝ) (↑m : ℝ) (logb (↑m : ℝ) (↑n : ℝ) * s) ≤ 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have rw₃ : HPow.hPow (α := ℝ) (↑m : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ^ s ≤ 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ)) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) s
have rw₄ : HPow.hPow (α := ℝ) (↑n : ℝ) s ≤ 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ f.IsEquiv real
have obtain : ∀ (m : ℕ) (hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)), f.IsEquiv real
Tactic: obtain ⟨m, hm⟩ := Classical.exists_not_of_not_forall notbdd
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ 1 < m
have contrapose! : ∀ (hm : m ≤ 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
Tactic: contrapose! hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : m ≤ 1
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have inl : ∀ (hm : LE.le (α := ℕ) 0 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑0 : ℚ) : ℝ) (1 : ℝ)
Tactic: rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have inr : ∀ (hm : LE.le (α := ℕ) 1 1), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) (1 : ℝ)
Tactic: rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ f.IsEquiv real
have oneltm : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
⊢ f.IsEquiv real
have rw : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (real : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: rw [← exists_nat_rpow_iff_isEquiv]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
m : ℕ
hm : ¬LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
oneltm : 1 < m
⊢ ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) c = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have hs : let s := logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ));
s = logb (↑m : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
Tactic: set s := logb m (f m) with hs
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
have refine : ∀ (n : ℕ), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℕ
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have inl : ∀ (h : n < 1), HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
Tactic: rcases lt_trichotomy n 1 with h | rfl | h
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑n : ℚ)
have inr : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ) s⁻¹ = (real : (a : ℚ) → ℝ) (↑1 : ℚ)
Tactic: rcases lt_trichotomy n 1 with h | rfl | h
Cleared hypotheses: n