-- Mathlib/NumberTheory/Ostrowski.lean
/-- If `f n > 1` for some `n` then `f n > 1` for all `n ≥ 2` -/
lemma one_lt_of_not_bounded (notbdd : ¬ ∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (hn₀ : 1 < n₀) : 1 < f n₀

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ ↑n₀ * f ↑n₀ ^ (i, a).2 ≤ ↑n₀

Tactic:
simp only [Function.comp_apply, Function.uncurry_apply_pair]

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
x✝¹ : ℕ × ℕ
i a : ℕ
x✝ : (i, a) ∈ L.zipIdx
⊢ ↑n₀ * f ↑n₀ ^ a ≤ ↑n₀

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹

Tactic:
rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
  mul_comm _ (k : ℝ)]

Result:
no goals

Proof state:
case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
⊢ f ↑n ≤ 1

Tactic:
rcases eq_or_ne n 1 with rfl | h₁

Result:
case inr.inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : 1 ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑1 ≤ (↑n₀ * (logb ↑n₀ ↑1 + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
⊢ f ↑1 ≤ 1

case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ f ↑n ≤ 1

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.mapIdx (fun x x => ↑n₀) L).sum = ↑n₀ * (↑(Nat.log n₀ m) + 1)

Tactic:
rw [List.mapIdx_eq_zipIdx_map, List.eq_replicate_of_mem (a := (n₀ : ℝ)) (l := L.zipIdx.map _),
  List.sum_replicate, List.length_map, List.length_zipIdx, nsmul_eq_mul, mul_comm,
  Nat.digits_len n₀ m hn₀ (not_eq_zero_of_lt hm), Nat.cast_add_one]

Result:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ∀
    b ∈
      List.map
        (fun x =>
          match x with
          | (a, i) => ↑n₀)
        L.zipIdx,
    b = ↑n₀

Proof state:
case inr.inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : 1 ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑1 ≤ (↑n₀ * (logb ↑n₀ ↑1 + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
⊢ f ↑1 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
case h₁
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ f ↑(n ^ k) ≤ ↑n₀ * (logb ↑n₀ ↑(n ^ k) + 1)

Tactic:
exact h_ineq1 <| one_le_pow₀ (one_le_iff_ne_zero.mpr h₀)

Result:
no goals

Proof state:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ↑n₀ * (↑(Nat.log n₀ m) + 1) ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)

Tactic:
gcongr

Result:
case h.bc
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ ↑(Nat.log n₀ m) ≤ logb ↑n₀ ↑m