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

Proof state:
case intro.inr.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)
⊢ f ↑1 ^ s⁻¹ = real ↑1

Tactic:
simp

Result:
no goals

Proof state:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
⊢ f ≈ real

Tactic:
have oneltm : 1 < m := by
  contrapose! hm
  rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl <;> simp

Result:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
⊢ f ≈ real

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
⊢ f ↑m = ↑m ^ s

Tactic:
rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]

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
⊢ f ↑n ^ s⁻¹ = ↑n

Tactic:
rw [rpow_inv_eq (apply_nonneg f ↑n) (Nat.cast_nonneg n)
  (logb_ne_zero_of_pos_of_ne_one (one_lt_cast.mpr oneltm) (by linarith only [hm])
  (by linarith only [hm]))]

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 = ↑n ^ logb (↑m) (f ↑m)

Proof state:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
oneltm : 1 < m
⊢ f ≈ real

Tactic:
rw [← equiv_on_nat_iff_equiv]

Result:
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

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
⊢ ¬↑m = -1

Tactic:
norm_cast

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)
h : 0 < 1
⊢ ¬m = 0 ∧ ¬m = 1 ∧ ¬↑m = -1 ∧ ¬m = 0 ∧ ¬f ↑m = 1 ∧ ¬f ↑m = -1

Tactic:
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:
no goals

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)
n : ℕ
h : n < 1
⊢ f ↑n ^ s⁻¹ = real ↑n

Tactic:
obtain rfl : n = 0 := by omega

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
⊢ f ↑0 ^ s⁻¹ = real ↑0

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
⊢ f ≈ real

Tactic:
obtain ⟨m, hm⟩ := Classical.exists_not_of_not_forall notbdd

Result:
case intro
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
⊢ f ≈ real

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
⊢ f ↑m ≠ 1

Tactic:
linarith only [hm]

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
⊢ f ↑n = ↑n ^ logb (↑m) (f ↑m)

Tactic:
have hfm : f m = m ^ s := by
  rw [rpow_logb (mod_cast zero_lt_of_lt oneltm) (mod_cast oneltm.ne') (by linarith only [hm])]

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
hfm : f ↑m = ↑m ^ s
⊢ f ↑n = ↑n ^ logb (↑m) (f ↑m)

Proof state:
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

Tactic:
refine ⟨s⁻¹,
  inv_pos.mpr (logb_pos (Nat.one_lt_cast.mpr oneltm) (one_lt_of_not_bounded notbdd oneltm)),
  fun n ↦ ?_⟩

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)
n : ℕ
⊢ f ↑n ^ s⁻¹ = real ↑n

Proof state:
case hx
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
⊢ ↑n ≠ 0

Tactic:
exact_mod_cast not_eq_zero_of_lt h

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 : n < 1
⊢ n = 0

Tactic:
omega

Result:
no goals

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
this : (logb (↑m) (f ↑m))⁻¹ ≠ 0
⊢ f ↑0 ^ s⁻¹ = real ↑0

Tactic:
simp [hs, this]

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
⊢ 1 < m

Tactic:
contrapose! hm

Result:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : m ≤ 1
⊢ f ↑m ≤ 1

Proof state:
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)
n : ℕ
⊢ f ↑n ^ s⁻¹ = real ↑n

Tactic:
rcases lt_trichotomy n 1 with h | rfl | h

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)
n : ℕ
h : n < 1
⊢ f ↑n ^ s⁻¹ = real ↑n

case intro.inr.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)
⊢ f ↑1 ^ s⁻¹ = real ↑1

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

Proof state:
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : m ≤ 1
⊢ f ↑m ≤ 1

Tactic:
rcases le_one_iff_eq_zero_or_eq_one.mp hm with rfl | rfl <;> simp

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
⊢ 0 < f ↑n

Tactic:
apply map_pos_of_ne_zero

Result:
case hx
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
⊢ ↑n ≠ 0

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
⊢ f ↑n = ↑n ^ logb (↑m) (f ↑m)

Tactic:
have hfn : f n = n ^ logb n (f n) := by
  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:
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)