awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
⊢ False
have ha₀ : a ≠ 0
Tactic: obtain ⟨ha₀, hb₀⟩ : a ≠ 0 ∧ b ≠ 0 := by
      refine mul_ne_zero_iff.mp fun h ↦ ?_
      rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
⊢ False
have hb₀ : b ≠ 0
Tactic: obtain ⟨ha₀, hb₀⟩ : a ≠ 0 ∧ b ≠ 0 := by
      refine mul_ne_zero_iff.mp fun h ↦ ?_
      rwa [h, Nat.cast_zero, map_zero, lt_self_iff_false] at hp0
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
⊢ False
have hap : a < a * b
Tactic: have hap : a < a * b := lt_mul_of_one_lt_right (by lia) (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
⊢ False
have hbp : b < a * b
Tactic: have hbp : b < a * b := lt_mul_of_one_lt_left (by lia) (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
⊢ False
have ha : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
Tactic: have ha :=
      le_of_not_gt <| not_and.mp ((hmin a).mt hap.not_ge) (map_pos_of_ne_zero f (mod_cast ha₀))
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
⊢ False
have hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
Tactic: have hb :=
      le_of_not_gt <| not_and.mp ((hmin b).mt hbp.not_ge) (map_pos_of_ne_zero f (mod_cast hb₀))
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (hypothesis)
Goal:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ)
hp1 : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑(a * b) : ℚ) : ℝ) (1 : ℝ)
hmin :
  ∀ (m : ℕ),
    LT.lt (α := ℝ) (0 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) ∧ LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ) →
      a * b ≤ m
ha₁ : a ≠ 1
hb₁ : b ≠ 1
ha₀ : a ≠ 0
hb₀ : b ≠ 0
hap : a < a * b
hbp : b < a * b
ha : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ)
hb : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ)
⊢ False
have hp1₁ : HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : ℚ) → ℝ) (↑a : ℚ) : ℝ) ((f : (a : ℚ) → ℝ) (↑b : ℚ) : ℝ) < 1
Tactic: rw [Nat.cast_mul, map_mul] at hp1
Cleared hypotheses: hp1, hmin, ha₁, hb₁, ha₀, hb₀, hap, hbp, ha, hb
-- 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
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)
have apply : LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
Tactic: apply le_antisymm (bdd m)
-- 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
⊢ LE.le (α := ℝ) (1 : ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ)
have by_contra! : ∀ (hm : LT.lt (α := ℝ) ((f : (a : ℚ) → ℝ) (↑m : ℚ) : ℝ) (1 : ℝ)), False
Tactic: by_contra! hm
-- 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 : ℝ)
⊢ False
have hM : 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
-- 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 : ℚ))
⊢ False
have hk : 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
-- 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
⊢ False
have obtain : ∀ (a b : ℤ) (bezout : a * HPow.hPow (α := ℤ) (↑p : ℤ) k + b * HPow.hPow (α := ℤ) (↑m : ℤ) k = 1), 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
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ HPow.hPow (β := ℝ) x (↑k : ℝ) < x ^ logb M (1 / 2)
have apply : logb M (1 / 2) < (↑k : ℝ)
Tactic: apply rpow_lt_rpow_of_exponent_gt hx0 hx1
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < (↑(⌈logb M (1 / 2)⌉₊ + 1) : ℝ)
have push_cast : logb M (1 / 2) < HAdd.hAdd (α := ℝ) (↑⌈logb M (1 / 2)⌉₊ : ℝ) 1
Tactic: push_cast
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)
have apply : logb x (1 / 2) ≤ logb M (1 / 2)
Tactic: apply rpow_le_rpow_of_exponent_ge hx0 hx1.le
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb x (1 / 2) ≤ logb M (1 / 2)
have simp : Real.log 2 / -Real.log x ≤ Real.log 2 / -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
Tactic: simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ Real.log 2 / -Real.log x ≤ Real.log 2 / -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
have hd : 0 < -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ 0 < -Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ)))
have hd : Real.log (max ((f : (a : ℚ) → ℝ) (↑p : ℚ)) ((f : (a : ℚ) → ℝ) (↑m : ℚ))) < 0
Tactic: simp only [Left.neg_pos_iff]
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ k < 1 / 2
have x₁ : HPow.hPow (β := ℝ) x (↑k : ℝ) < x ^ logb M (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
-- 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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
x₁ : HPow.hPow (β := ℝ) x (↑k : ℝ) < x ^ logb M (1 / 2)
⊢ x ^ k < 1 / 2
have x₂ : x ^ logb M (1 / 2) ≤ x ^ logb x (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
-- 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
⊢ False
have le_half : ∀ {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
-- 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
⊢ False
have apply : LT.lt (α := ℝ) 1 1
Tactic: apply lt_irrefl (1 : ℝ)
-- 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
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
    ((f : (a : ℚ) → ℝ) ((↑a : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) k + (↑b : ℚ) * HPow.hPow (α := ℚ) (↑m : ℚ) k) : ℝ)
have 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 : ℚ) : ℝ)
Tactic: rw_mod_cast [bezout]
Cleared hypotheses: bdd, hp0, hp1, hmin, hm, hk, bezout, le_half
-- Lean 4 proof step from Mathlib.NumberTheory.Ostrowski (goal)
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
⊢ Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ) ((f : (a : ℚ) → ℝ) (↑1 : ℚ) : ℝ)
have norm_cast : Eq (α := ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ) ((f : (a : ℚ) → ℝ) 1 : ℝ)
Tactic: norm_cast