-- Mathlib/NumberTheory/Ostrowski.lean
theorem equiv_real_of_unbounded : f ≈ real

Proof state:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = real ↑n

Tactic:
set s := logb m (f m) with hs

Result:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
⊢ ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = real ↑n

Proof state:
case intro.inr.inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
n : ℕ
h : 1 < n
⊢ f ↑n ^ s⁻¹ = real ↑n

Tactic:
simp only [real_eq_abs, abs_cast, Rat.cast_natCast]

Result:
case intro.inr.inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
n : ℕ
h : 1 < n
⊢ f ↑n ^ s⁻¹ = ↑n

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
h : 0 < 1
⊢ (logb (↑m) (f ↑m))⁻¹ ≠ 0

Tactic:
simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
  not_or]

Result:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
h : 0 < 1
⊢ ¬m = 0 ∧ ¬m = 1 ∧ ¬↑m = -1 ∧ ¬m = 0 ∧ ¬f ↑m = 1 ∧ ¬f ↑m = -1

Proof state:
case intro.inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
h : 0 < 1
⊢ f ↑0 ^ s⁻¹ = real ↑0

Tactic:
have : (logb (↑m) (f ↑m))⁻¹ ≠ 0 := by
  simp only [ne_eq, inv_eq_zero, logb_eq_zero, Nat.cast_eq_zero, Nat.cast_eq_one, map_eq_zero,
    not_or]
  exact ⟨not_eq_zero_of_lt oneltm, oneltm.ne', by norm_cast,
    not_eq_zero_of_lt oneltm, ne_of_not_le hm, by linarith only [apply_nonneg f ↑m]⟩

Result:
case intro.inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
h : 0 < 1
this : (logb (↑m) (f ↑m))⁻¹ ≠ 0
⊢ f ↑0 ^ s⁻¹ = real ↑0

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
h : 0 < 1
⊢ ¬f ↑m = -1

Tactic:
linarith only [apply_nonneg f ↑m]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
n : ℕ
h : 1 < n
hfm : f ↑m = ↑m ^ s
⊢ f ↑n = ↑n ^ logb (↑n) (f ↑n)

Tactic:
rw [rpow_logb (mod_cast zero_lt_of_lt h) (mod_cast h.ne')
  (by apply map_pos_of_ne_zero; exact_mod_cast not_eq_zero_of_lt h)]

Result:
no goals

Proof state:
case intro.inr.inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
n : ℕ
h : 1 < n
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ logb (↑n) (f ↑n)
⊢ f ↑n = ↑n ^ logb (↑m) (f ↑m)

Tactic:
rwa [← hs, eq_of_eq_pow oneltm h notbdd hfm hfn]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
n : ℕ
h : 1 < n
⊢ 0 < f ↑m

Tactic:
linarith only [hm]

Result:
no goals