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
apply : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)

Tactic:
apply le_antisymm (bdd m)

Premises used: le_antisymm
-- 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
by_contra! : ∀ (hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)), False
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)

Tactic:
by_contra! hm
-- 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 : ℝ)
⊢ let M : ℝ := max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ));
  M = max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))

Tactic:
set M := f p ⊔ f m with hM

Premises used: Nat.cast, DFunLike.coe
-- 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 : ℚ))
⊢ let k := ⌈logb M (1 / 2)⌉₊ + 1;
  k = ⌈logb M (1 / 2)⌉₊ + 1

Tactic:
set k := Nat.ceil (M.logb (1 / 2)) + 1 with hk

Premises used: HDiv.hDiv, Real.logb, Nat.ceil, OfNat.ofNat
-- 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
⊢ IsCoprime (HPow.hPow (α := ℤ) (↑p : ℤ) k) (HPow.hPow (α := ℤ) (↑m : ℤ) k)

Tactic:
is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin
      |>.coprime_iff_not_dvd |>.mpr hpm |>.isCoprime |>.pow

Premises used: Iff.mpr, Rat.AbsoluteValue.is_prime_of_minimal_nat_zero_lt_and_lt_one, IsCoprime.pow, Nat.Prime.coprime_iff_not_dvd, Nat.Coprime.isCoprime
-- 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
obtain : ∀ (a b : ℤ) (bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1), False
⊢ False

Tactic:
obtain ⟨a, b, bezout⟩ : IsCoprime (p ^ k : ℤ) (m ^ k) :=
    is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin
      |>.coprime_iff_not_dvd |>.mpr hpm |>.isCoprime |>.pow

Premises used: Iff.mpr, Rat.AbsoluteValue.is_prime_of_minimal_nat_zero_lt_and_lt_one, Nat.cast, HPow.hPow, IsCoprime.pow, Nat.Prime.coprime_iff_not_dvd, Nat.Coprime.isCoprime, IsCoprime
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ k = HPow.hPow (β := ℝ) x (↑k : ℝ)

Tactic:
(rpow_natCast x k).symm

Premises used: Eq.symm, Real.rpow_natCast
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
apply : logb M (1 / 2) < (↑k : ℝ)
⊢ HPow.hPow (β := ℝ) x (↑k : ℝ) < x ^ logb M (1 / 2)

Tactic:
apply rpow_lt_rpow_of_exponent_gt hx0 hx1

Premises used: Real.rpow_lt_rpow_of_exponent_gt
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
rw : logb M (1 / 2) < (↑(⌈logb M (1 / 2)⌉₊ + 1) : ℝ)
⊢ logb M (1 / 2) < (↑k : ℝ)

Tactic:
rw [hk]
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
push_cast : logb M (1 / 2) < HAdd.hAdd (α := ℝ) (↑⌈logb M (1 / 2)⌉₊ : ℝ) 1
⊢ logb M (1 / 2) < (↑(⌈logb M (1 / 2)⌉₊ + 1) : ℝ)

Tactic:
push_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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < HAdd.hAdd (α := ℝ) (↑⌈logb M (1 / 2)⌉₊ : ℝ) 1

Tactic:
lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one

Premises used: zero_lt_one, lt_add_of_le_of_pos, Nat.le_ceil
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < HAdd.hAdd (α := ℝ) (↑⌈logb M (1 / 2)⌉₊ : ℝ) 1

Tactic:
exact lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one

Premises used: zero_lt_one, lt_add_of_le_of_pos, Nat.le_ceil
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
apply : logb x (1 / 2) ≤ logb M (1 / 2)
⊢ x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)

Tactic:
apply rpow_le_rpow_of_exponent_ge hx0 hx1.le

Premises used: LT.lt.le, Real.rpow_le_rpow_of_exponent_ge
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
simp : Real.log 2 / -Real.log x ≤ Real.log 2 / -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
⊢ logb x (1 / 2) ≤ logb M (1 / 2)

Tactic:
simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]

Premises used: neg_div, Real.log_div_log, div_neg, one_div, Real.log_inv
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
hd : 0 < -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
⊢ Real.log 2 / -Real.log x ≤ Real.log 2 / -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))

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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
hd : Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))) < 0
⊢ 0 < -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))

Tactic:
simp only [Left.neg_pos_iff]

Premises used: Left.neg_pos_iff
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))) < 0

Tactic:
log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)

Premises used: Iff.mpr, lt_sup_iff, sup_lt_iff, And.intro, Or.inl, Real.log_neg
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))) < 0

Tactic:
exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)

Premises used: Iff.mpr, lt_sup_iff, sup_lt_iff, And.intro, Or.inl, Real.log_neg
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ logb x (1 / 2) = 1 / 2

Tactic:
rpow_logb hx0 hx1.ne one_half_pos

Premises used: Real.rpow_logb, one_half_pos, LT.lt.ne
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
x₁ : HPow.hPow (β := ℝ) x (↑k : ℝ) < x ^ logb M (1 / 2)
x₂ : x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)
⊢ x ^ k < 1 / 2

Tactic:
calc
    x ^ k = x ^ (k : ℝ) := (rpow_natCast x k).symm
    _ < x ^ M.logb (1 / 2) := by
      apply rpow_lt_rpow_of_exponent_gt hx0 hx1
      rw [hk]
      push_cast
      exact lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one
    _ ≤ x ^ x.logb (1 / 2) := by
      apply rpow_le_rpow_of_exponent_ge hx0 hx1.le
      simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]
      gcongr
      simp only [Left.neg_pos_iff]
      exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)
    _ = 1 / 2 := rpow_logb hx0 hx1.ne one_half_pos

Premises used: HDiv.hDiv, Nat.cast, Real.rpow_logb, Real.logb, one_half_pos, OfNat.ofNat, Eq.symm, Real.rpow_natCast, LT.lt.ne
-- 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
⊢ ∀ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M), x ^ k < 1 / 2

Tactic:
have le_half {x} (hx0 : 0 < x) (hx1 : x < 1) (hxM : x ≤ M) : x ^ k < 1 / 2 := by
    calc
    x ^ k = x ^ (k : ℝ) := (rpow_natCast x k).symm
    _ < x ^ M.logb (1 / 2) := by
      apply rpow_lt_rpow_of_exponent_gt hx0 hx1
      rw [hk]
      push_cast
      exact lt_add_of_le_of_pos (Nat.le_ceil _) zero_lt_one
    _ ≤ x ^ x.logb (1 / 2) := by
      apply rpow_le_rpow_of_exponent_ge hx0 hx1.le
      simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]
      gcongr
      simp only [Left.neg_pos_iff]
      exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)
    _ = 1 / 2 := rpow_logb hx0 hx1.ne one_half_pos
-- 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
apply : LT.lt (α := ℝ) 1 1
⊢ False

Tactic:
apply lt_irrefl (1 : ℝ)

Premises used: lt_irrefl, OfNat.ofNat
-- 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
⊢ Eq (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)

Tactic:
(map_one f).symm

Premises used: map_one, Eq.symm