-- Mathlib/NumberTheory/Ostrowski.lean
/-- A natural number not divible by `p` has absolute value 1. -/
lemma eq_one_of_not_dvd {m : ℕ} (hpm : ¬ p ∣ m) : f m = 1

Proof state:
case h₂.h
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑b ≤ 1

Tactic:
rw [← apply_natAbs_eq]

Result:
case h₂.h
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑b.natAbs ≤ 1

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
⊢ False

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

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑(⌈logb M (1 / 2)⌉₊ + 1)

Tactic:
push_cast

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb M (1 / 2) < ↑⌈logb M (1 / 2)⌉₊ + 1

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑p ^ k + f ↑m ^ k < 1

Tactic:
have hm₀ : 0 < f m := f.pos <| Nat.cast_ne_zero.mpr fun H ↦ hpm <| H ▸ dvd_zero p

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
hm₀ : 0 < f ↑m
⊢ f ↑p ^ k + f ↑m ^ k < 1

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ 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

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
⊢ 1 ≤ f ↑m

Tactic:
by_contra! hm

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
⊢ False

Proof state:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)

Tactic:
apply rpow_le_rpow_of_exponent_ge hx0 hx1.le

Result:
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ logb x (1 / 2) ≤ logb M (1 / 2)

Proof state:
case h₁.h
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑a ≤ 1

case h₂.h
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := f ↑p ⊔ f ↑m
hM : M = f ↑p ⊔ f ↑m
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑b ≤ 1

Tactic:
all_goals rw [← apply_natAbs_eq]; apply bdd

Result:
no goals