awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
rw_mod_cast :
  ∀ (bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ))
    (hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ))
    (hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m)
    (hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)) (hk : k = ⌈logb M (HDiv.hDiv (α := ℝ) 1 2)⌉₊ + 1)
    (bezout : a * (↑(p ^ k) : ℤ) + b * (↑(m ^ k) : ℤ) = 1)
    (le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < HDiv.hDiv (α := ℝ) 1 2),
    Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
    ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k + (↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ)

Tactic:
rw_mod_cast [bezout]
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p m : ℕ
hpm : ¬p ∣ m
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
hk : k = ⌈logb M (HDiv.hDiv (α := ℝ) 1 2)⌉₊ + 1
bezout : a * (↑(p ^ k) : ℤ) + b * (↑(m ^ k) : ℤ) = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < HDiv.hDiv (α := ℝ) 1 2
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
⊢ (f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k + (↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k) : ℝ)
      ((f : (a : ℚ) → ℝ) ((↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ)

Tactic:
f.add_le' ..

Premises used: AbsoluteValue.add_le'
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
simp :
  HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k) +
      HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k) ≤
    1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k) : ℝ)
      ((f : (a : ℚ) → ℝ) ((↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ) ≤
    1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k

Tactic:
simp only [map_mul, map_pow]

Premises used: map_pow, map_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
h₁ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (1 : ℝ)
h₂ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) (1 : ℝ)
⊢ HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k) +
      HMul.hMul (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k) ≤
    1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
h₁ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a.natAbs : ℚ) : ℝ) (1 : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (1 : ℝ)

Tactic:
rw [← apply_natAbs_eq]

Premises used: AbsoluteValue.apply_natAbs_eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a.natAbs : ℚ) : ℝ) (1 : ℝ)

Tactic:
apply bdd
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
h₂ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b.natAbs : ℚ) : ℝ) (1 : ℝ)
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) (1 : ℝ)

Tactic:
rw [← apply_natAbs_eq]

Premises used: AbsoluteValue.apply_natAbs_eq
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
⊢ LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b.natAbs : ℚ) : ℝ) (1 : ℝ)

Tactic:
apply bdd
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
⊢ 1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k =
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k

Tactic:
simp only [one_mul]

Premises used: one_mul
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
⊢ LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)

Tactic:
have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
hm₀ : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
linarith :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    2 / 2 = 1
linarith₁ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    GT.gt (α := ℝ) 2 0
linarith₃ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    2 / 2 = 1
linarith₄ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    GT.gt (α := ℝ) 2 0
linarith₆ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    2 *
            (1 -
              (HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
                HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k)) +
          (2 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k - HMul.hMul (α := ℝ) 1 1) +
        (2 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k - HMul.hMul (α := ℝ) 1 1) =
      0
linarith₇ :
  1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
    GT.gt (α := ℝ) 2 0
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1

Tactic:
linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]

Premises used: le_sup_left, le_sup_right
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
hM : M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1
le_half : ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2
f₁ :
  Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
    ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k + (↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ)
f₂ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k) : ℝ)
      ((f : (a : ℚ) → ℝ) ((↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ) ≤
    1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k
f₃ :
  1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k +
      1 * HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k =
    HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k
f₄ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
⊢ LT.lt (α := ℝ) 1 1

Tactic:
calc
  1 = f 1 := (map_one f).symm
  _ = f (a * p ^ k + b * m ^ k) := by rw_mod_cast [bezout]; norm_cast
  _ ≤ f (a * p ^ k) + f (b * m ^ k) := f.add_le' ..
  _ ≤ 1 * (f p) ^ k + 1 * (f m) ^ k := by
    simp only [map_mul, map_pow]
    gcongr
    all_goals rw [← apply_natAbs_eq]; apply bdd
  _ = (f p) ^ k + (f m) ^ k := by simp only [one_mul]
  _ < 1 := by
    have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p
    linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]

Premises used: Int.cast, HMul.hMul, Nat.cast, HPow.hPow, HAdd.hAdd, map_one, OfNat.ofNat, Eq.symm, DFunLike.coe, AbsoluteValue.add_le'
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
⊢ Nat.Prime p

Tactic:
have pprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
pprime : Nat.Prime p
⊢ ∃ (t : ℝ), 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)

Tactic:
⟨- logb p (f p), Left.neg_pos_iff.mpr <| logb_neg (mod_cast pprime.one_lt) hp0 hp1, ?_⟩

Premises used: Iff.mpr, Nat.Prime.one_lt, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, Real.logb, Left.neg_pos_iff, And.intro, LT.lt, Exists.intro, congrFun', Real.logb_neg, Eq.symm, Nat.cast_one, DFunLike.coe, Neg.neg, Eq.trans
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
pprime : Nat.Prime p
refine : (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))
⊢ ∃ (t : ℝ), 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)

Tactic:
refine ⟨- logb p (f p), Left.neg_pos_iff.mpr <| logb_neg (mod_cast pprime.one_lt) hp0 hp1, ?_⟩
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
pprime : Nat.Prime p
rw : (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))
⊢ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))

Tactic:
rw [neg_neg]

Premises used: neg_neg
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
pprime : Nat.Prime p
⊢ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))

Tactic:
(rpow_logb (mod_cast pprime.pos) (mod_cast pprime.ne_one) hp0).symm

Premises used: Real.rpow_logb, Eq.symm
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
pprime : Nat.Prime p
⊢ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))

Tactic:
exact (rpow_logb (mod_cast pprime.pos) (mod_cast pprime.ne_one) hp0).symm

Premises used: Real.rpow_logb, Eq.symm
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
obtain :
  ∀ (p : ℕ)
    (hfp :
      LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ))
    (hmin :
      ∀ (m : ℕ),
        LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧
            LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
          p ≤ m),
    ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)
⊢ ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)

Tactic:
obtain ⟨p, hfp, hmin⟩ := exists_minimal_nat_zero_lt_and_lt_one hf_nontriv bdd

Premises used: Rat.AbsoluteValue.exists_minimal_nat_zero_lt_and_lt_one
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
⊢ Nat.Prime p

Tactic:
have hprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hfp.1 hfp.2 hmin
-- Module: Mathlib.NumberTheory.Ostrowski
Goal:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑n : ℚ) : ℝ) (1 : ℝ)
p : ℕ
hfp : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      p ≤ m
hprime : Nat.Prime p
⊢ Fact (Nat.Prime p)

Tactic:
have hprime_fact : Fact p.Prime := ⟨hprime⟩