awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ 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
have 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
Tactic: simp only [map_mul, map_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ 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
have h₁ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) (1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℝ)
⊢ 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
have h₂ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) (1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) : ℝ) (1 : ℝ)
have h₁ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑a.natAbs : ℚ) : ℝ) (1 : ℝ)
Tactic: rw [← apply_natAbs_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) : ℝ) (1 : ℝ)
have h₂ : LE.le (α := ℝ) ((f : (a : ℚ) → ℝ) (↑b.natAbs : ℚ) : ℝ) (1 : ℝ)
Tactic: rw [← apply_natAbs_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
have hm₀ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ) : ℝ)
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
have linarith : 1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
  2 / 2 = 1
Tactic: linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
have linarith₁ : 1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
  HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
have linarith₂ : 1 ≤ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k →
  GT.gt (α := ℝ) 2 0
Tactic: linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 1
have 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
Tactic: linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 (α := ℝ) 1 1
have f₁ : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
  ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k + (↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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) : ℝ)
⊢ LT.lt (α := ℝ) 1 1
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ LT.lt (α := ℝ) 1 1
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ LT.lt (α := ℝ) 1 1
have f₄ : HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ) : ℝ) k + HPow.hPow (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) k < 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
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
⊢ ∃ (t : ℝ), 0 < t ∧ (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (-t)
have pprime : Nat.Prime p
Tactic: have pprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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)
have refine : (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (- -logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))
Tactic: refine ⟨- logb p (f p), Left.neg_pos_iff.mpr <| logb_neg (mod_cast pprime.one_lt) hp0 hp1, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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 : ℚ)))
have rw : (f : (a : ℚ) → ℝ) (↑p : ℚ) = HPow.hPow (α := ℝ) (↑p : ℝ) (logb (↑p : ℝ) ((f : (a : ℚ) → ℝ) (↑p : ℚ)))
Tactic: rw [neg_neg]