awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia : (a, i) ∈ L.zipIdx
⊢ (f : (a : ℚ) → ℝ) (↑(a * m ^ i) : ℚ) ≤ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
have hia₁ : 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) sorry
Tactic: replace hia := List.mem_zipIdx hia
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia_1 : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ (f : (a : ℚ) → ℝ) (↑(a * m ^ i) : ℚ) ≤ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
have push_cast : (f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) i) ≤
  (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia_1 : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ (f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
have rw : HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) ≤
  (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
Tactic: rw [map_mul, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia_1 : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
have refine : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
Tactic: refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hL' : L' = List.map Nat.cast (List.mapIdx (fun (i a : ℕ) ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ} (hc : c ∈ m.digits n), LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑c : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
x : ℕ × ℕ
a i : ℕ
hia_1 : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
have hia₁ : i < L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) sorry
Tactic: simp only [zero_le, zero_add, true_and] at hia
Cleared hypotheses: hia
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ 0 <
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have apply : 0 < HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
Tactic: apply div_pos (mul_pos (mod_cast hm.pos) (map_pos_of_ne_zero f (mod_cast hm.ne_zero)))
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have linarith : HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) ≤ 0 →
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) - 0 +
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
    0
Tactic: linarith only [one_lt_of_not_bounded notbdd hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
have rw : (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (m.digits n).length - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) =
  (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
Tactic: rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
rw :
  (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (m.digits n).length - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
⊢ HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
have rw₁ : (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (m.digits n).length - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) =
  (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (m.digits n).length - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
Tactic: rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) ≤
    (↑m : ℝ) *
      (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
have hbc : 0 ≤ HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hbc : 0 ≤ HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) ≤
    (↑m : ℝ) *
      (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
have hbc₁ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1 ≤
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ 0 ≤ HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have linarith : HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) < 0 →
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) - 0 +
      HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
    0
Tactic: linarith only [one_lt_of_not_bounded notbdd hm]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have ha : 0 ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
    HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
ha :
  0 ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have hbc : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have hbc : (↑d : ℝ) ≤ logb (↑m : ℝ) (↑n : ℝ)
Tactic: rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have f₁ : HMul.hMul (α := ℝ) (↑m : ℝ)
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
  (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
Tactic: calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr
      · linarith only [one_lt_of_not_bounded notbdd hm]
      · simp
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      · exact (expr_pos hm notbdd).le
      · rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
        exact natLog_le_logb n m
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
f₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have f₂ : (↑m : ℝ) *
    ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) ≤
  (↑m : ℝ) *
    (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
Tactic: calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr
      · linarith only [one_lt_of_not_bounded notbdd hm]
      · simp
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      · exact (expr_pos hm notbdd).le
      · rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
        exact natLog_le_logb n m
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
f₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
f₂ :
  (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) ≤
    (↑m : ℝ) *
      (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have f₃ : (↑m : ℝ) *
    (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) =
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d
Tactic: calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr
      · linarith only [one_lt_of_not_bounded notbdd hm]
      · simp
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      · exact (expr_pos hm notbdd).le
      · rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
        exact natLog_le_logb n m
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
Goal:
f : AbsoluteValue ℚ ℝ
m_1 n_1 : ℕ
hm_1 : 1 < m_1
hn_1 : 1 < n_1
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
f₁ :
  HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n))) =
    (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
f₂ :
  (↑m : ℝ) *
      ((HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) ≤
    (↑m : ℝ) *
      (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ))
f₃ :
  (↑m : ℝ) *
      (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) =
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
have f₄ : HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))
Tactic: calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr
      · linarith only [one_lt_of_not_bounded notbdd hm]
      · simp
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      · exact (expr_pos hm notbdd).le
      · rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
        exact natLog_le_logb n m
-- 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 : ℝ)
k : ℕ
hk : k ≠ 0
⊢ (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 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 : ℝ))
Tactic: have h_ineq1 {m n : ℕ} (hm : 1 < m) (hn : 1 < n) :
      f n ≤ (m * f m / (f m - 1)) * f m ^ logb m n := by
    let d := Nat.log m n
    calc
    f n ≤ ((Nat.digits m n).mapIdx fun i _ ↦ m * f m ^ i).sum := apply_le_sum_digits n hm
    _ = m * ((Nat.digits m n).mapIdx fun i _ ↦ f m ^ i).sum := list_mul_sum (m.digits n) (f m) m
    _ = m * ((f m ^ (d + 1) - 1) / (f m - 1)) := by
      rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]
    _ ≤ m * ((f m ^ (d + 1)) / (f m - 1)) := by
      gcongr
      · linarith only [one_lt_of_not_bounded notbdd hm]
      · simp
    _ = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d := by ring
    _ ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n := by
      gcongr
      · exact (expr_pos hm notbdd).le
      · rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]
        exact natLog_le_logb n m