awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ) : ℝ)
simp :
  LE.le (α := ℝ)
    (List.sum
      (List.map (Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2)) L.zipIdx))
    (List.sum
      (List.map (fun (x : ℕ × ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) x.2) L.zipIdx))
⊢ LE.le (α := ℝ) (List.sum (List.map (⇑f : (a : ℚ) → ℝ) L'))
    (List.sum (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) L))

Tactic:
simp only [hL', List.mapIdx_eq_zipIdx_map, List.map_map]

Premises used: List.map_map, List.mapIdx_eq_zipIdx_map
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ) : ℝ)
⊢ LE.le (α := ℝ)
    (List.sum
      (List.map (Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2)) L.zipIdx))
    (List.sum
      (List.map (fun (x : ℕ × ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) x.2) L.zipIdx))

Tactic:
List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_

Premises used: HMul.hMul, List.sum_le_sum, Function.comp, LE.le, Nat.cast, Prod.fst, HPow.hPow, _private.0.Rat.AbsoluteValue.apply_le_sum_digits.match_1, Prod.snd, DFunLike.coe
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ) : ℝ)
refine :
  ∀ (x : ℕ × ℕ) (a i : ℕ) (hia : (a, i) ∈ L.zipIdx),
    Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2) (a, i) ≤
      (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (a, i).2
⊢ LE.le (α := ℝ)
    (List.sum
      (List.map (Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2)) L.zipIdx))
    (List.sum
      (List.map (fun (x : ℕ × ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) x.2) L.zipIdx))

Tactic:
refine List.sum_le_sum fun ⟨a, i⟩ hia ↦ ?_

Premises used: List.sum_le_sum
-- Module: Mathlib.NumberTheory.Ostrowski
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
dsimp : (f : (a : ℚ) → ℝ) (↑(a * m ^ i) : ℚ) ≤ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
⊢ Function.comp (β := ℚ) (⇑f : (a : ℚ) → ℝ) (Nat.cast ∘ fun (x : ℕ × ℕ) ↦ x.1 * m ^ x.2) (a, i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (a, i).2

Tactic:
dsimp only [Function.comp_apply, Function.uncurry_apply_pair]

Premises used: Function.comp_apply, Function.uncurry_apply_pair
-- Module: Mathlib.NumberTheory.Ostrowski
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
⊢ 0 ≤ i ∧ i < 0 + L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯

Tactic:
replace hia := List.mem_zipIdx hia
-- Module: Mathlib.NumberTheory.Ostrowski
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) ⋯
push_cast :
  (f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
⊢ (f : (a : ℚ) → ℝ) (↑(a * m ^ i) : ℚ) ≤ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Ostrowski
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) ⋯
rw :
  HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i
⊢ (f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i

Tactic:
rw [map_mul, map_pow]

Premises used: map_pow, map_mul
-- Module: Mathlib.NumberTheory.Ostrowski
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

Tactic:
mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i

Premises used: pow_nonneg, AbsoluteValue.nonneg, mul_le_mul_of_nonneg_right
-- Module: Mathlib.NumberTheory.Ostrowski
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) ⋯
refine : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((↑m : ℝ) : ℝ)
⊢ HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) ≤
    (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i

Tactic:
refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i

Premises used: pow_nonneg, AbsoluteValue.nonneg, mul_le_mul_of_nonneg_right
-- Module: Mathlib.NumberTheory.Ostrowski
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) ⋯
⊢ i < L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯

Tactic:
simp only [zero_le, zero_add, true_and] at hia

Premises used: Nat.zero_le, zero_add, true_and
-- Module: Mathlib.NumberTheory.Ostrowski
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 : i < L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((↑m : ℝ) : ℝ)

Tactic:
(hcoef (List.mem_iff_get.mpr ⟨⟨i, hia.1⟩, hia.2.symm⟩)).le

Premises used: Iff.mpr, List.mem_iff_get, Fin.mk, LT.lt.le, And.right, And.left, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Ostrowski
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 : i < L.length ∧ a = getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L (i - 0) ⋯
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((↑m : ℝ) : ℝ)

Tactic:
exact (hcoef (List.mem_iff_get.mpr ⟨⟨i, hia.1⟩, hia.2.symm⟩)).le

Premises used: Iff.mpr, List.mem_iff_get, Fin.mk, LT.lt.le, And.right, And.left, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
apply : 0 < HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
⊢ 0 <
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      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)))

Premises used: map_pos_of_ne_zero, mul_pos, div_pos
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
m : ℕ
hm : 1 < m
notbdd : ¬∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
linarith :
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) ≤ 0 →
    HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) - 0 +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
      0
⊢ 0 < HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
linarith only [one_lt_of_not_bounded notbdd hm]

Premises used: Rat.AbsoluteValue.one_lt_of_not_bounded
-- Module: Mathlib.NumberTheory.Ostrowski
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
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ)
    (List.sum
        (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n)) :
      ℝ)

Tactic:
apply_le_sum_digits n hm

Premises used: Rat.AbsoluteValue.apply_le_sum_digits
-- Module: Mathlib.NumberTheory.Ostrowski
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
⊢ List.sum
      (List.mapIdx (fun (i x : ℕ) ↦ (↑m : ℝ) * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n)) =
    HMul.hMul (α := ℝ) (↑m : ℝ)
      (List.sum (List.mapIdx (fun (i x : ℕ) ↦ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) i) (m.digits n)))

Tactic:
list_mul_sum (m.digits n) (f m) m

Premises used: Nat.cast, _private.0.list_mul_sum, Nat.digits, DFunLike.coe
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ))
rw₁ 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 : ℝ))
⊢ 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:
rw [list_geom _ (ne_of_gt (one_lt_of_not_bounded notbdd hm)),
        ← Nat.length_digits m n hm (ne_zero_of_lt hn)]

Premises used: _private.0.list_geom, ne_zero_of_lt, ne_of_gt, Nat.length_digits, Rat.AbsoluteValue.one_lt_of_not_bounded
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ)
hbc₁ :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1) - 1 ≤
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 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 : ℝ))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Ostrowski
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
linarith :
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) < 0 →
    HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) - 0 +
        HSub.hSub (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) =
      0
⊢ 0 ≤ HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
linarith only [one_lt_of_not_bounded notbdd hm]

Premises used: Rat.AbsoluteValue.one_lt_of_not_bounded
-- Module: Mathlib.NumberTheory.Ostrowski
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 + 1) - 1 ≤
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (d + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Ostrowski
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) /
        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:
ring
-- Module: Mathlib.NumberTheory.Ostrowski
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 : ℝ)
hbc :
  HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
    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 : ℚ) : ℝ) d ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
        HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) *
      HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Ostrowski
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 ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
(expr_pos hm notbdd).le

Premises used: LT.lt.le, _private.0.Rat.AbsoluteValue.expr_pos
-- Module: Mathlib.NumberTheory.Ostrowski
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 ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) /
      HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
exact (expr_pos hm notbdd).le

Premises used: LT.lt.le, _private.0.Rat.AbsoluteValue.expr_pos
-- Module: Mathlib.NumberTheory.Ostrowski
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 : (↑d : ℝ) ≤ logb (↑m : ℝ) (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) d ≤
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (logb (↑m : ℝ) (↑n : ℝ))

Tactic:
rw [← rpow_natCast, rpow_le_rpow_left_iff (one_lt_of_not_bounded notbdd hm)]

Premises used: Real.rpow_le_rpow_left_iff, Rat.AbsoluteValue.one_lt_of_not_bounded, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Ostrowski
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
⊢ (↑d : ℝ) ≤ logb (↑m : ℝ) (↑n : ℝ)

Tactic:
natLog_le_logb n m

Premises used: Real.natLog_le_logb
-- Module: Mathlib.NumberTheory.Ostrowski
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
⊢ (↑d : ℝ) ≤ logb (↑m : ℝ) (↑n : ℝ)

Tactic:
exact natLog_le_logb n m

Premises used: Real.natLog_le_logb
-- Module: Mathlib.NumberTheory.Ostrowski
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₄ :
  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 : ℝ))
⊢ (f : (a : ℚ) → ℝ) (↑n : ℚ) ≤
    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

Premises used: List.mapIdx, HMul.hMul, List.sum, HSub.hSub, HDiv.hDiv, Nat.cast, Real.logb, HPow.hPow, HAdd.hAdd, _private.0.list_mul_sum, Nat.digits, OfNat.ofNat, DFunLike.coe, Rat.AbsoluteValue.apply_le_sum_digits
-- 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
⊢ ∀ {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