-- Mathlib/Data/Real/Archimedean.lean
/-- Exponentiation is eventually larger than linear growth. -/
lemma exists_natCast_add_one_lt_pow_of_one_lt (ha : 1 < a) : ∃ m : ℕ, (m + 1 : ℝ) < a ^ m

Proof state:
a : ℝ
ha : 1 < a
⊢ ∃ m, ↑m + 1 < a ^ m

Tactic:
obtain ⟨k, posk, hk⟩ : ∃ k : ℕ, 0 < k ∧ 1 / k + 1 < a := by
  contrapose! ha
  refine le_of_forall_lt_rat_imp_le ?_
  intro q hq
  refine (ha q.den (by positivity)).trans ?_
  rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]
  norm_cast at hq ⊢
  rw [← q.num_div_den, one_lt_div (by positivity)] at hq
  rw [q.mul_den_eq_num]
  norm_cast at hq ⊢
  omega

Result:
case intro.intro
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ∃ m, ↑m + 1 < a ^ m

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ((1 / ↑k + 1) ^ k) ^ (2 * k) = (1 / ↑k + 1) ^ (2 * k ^ 2)

Tactic:
rw [← pow_mul, mul_left_comm, sq]

Result:
no goals

Proof state:
a : ℝ
ha : 1 < a
⊢ ∃ k, 0 < k ∧ 1 / ↑k + 1 < a

Tactic:
contrapose! ha

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
⊢ a ≤ 1

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
⊢ ∀ (q : ℚ), 1 < ↑q → a ≤ ↑q

Tactic:
intro q hq

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ a ≤ ↑q

Proof state:
case intro.intro
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ∃ m, ↑m + 1 < a ^ m

Tactic:
use 2 * k ^ 2

Result:
case h
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ↑(2 * k ^ 2) + 1 < a ^ (2 * k ^ 2)

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 / ↑q.den + 1 ≤ ↑q

Tactic:
rw [← le_sub_iff_add_le, div_le_iff₀ (by positivity), sub_mul, one_mul]

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - ↑q.den

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < q.num
⊢ 1 ≤ q.num - ↑q.den

Tactic:
omega

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 0 < ↑q.den

Tactic:
positivity

Result:
no goals

Proof state:
case h
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ ↑(2 * k ^ 2) + 1 < a ^ (2 * k ^ 2)

Tactic:
calc
  ((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
  _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
  _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
  _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
  _ < a ^ (2 * k ^ 2) := by gcongr

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < q
⊢ 1 ≤ q * ↑q.den - ↑q.den

Tactic:
rw [← q.num_div_den, one_lt_div (by positivity)] at hq

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ q * ↑q.den - ↑q.den

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - ↑q.den

Tactic:
norm_cast at hq ⊢

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < q
⊢ 1 ≤ q * ↑q.den - ↑q.den

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ q * ↑q.den - ↑q.den

Tactic:
rw [q.mul_den_eq_num]

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ ↑q.num - ↑q.den

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
⊢ a ≤ 1

Tactic:
refine le_of_forall_lt_rat_imp_le ?_

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
⊢ ∀ (q : ℚ), 1 < ↑q → a ≤ ↑q

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ (1 / ↑k + 1) ^ (2 * k ^ 2) < a ^ (2 * k ^ 2)

Tactic:
gcongr

Result:
no goals

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1

Tactic:
norm_num

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ ↑q.num - ↑q.den

Tactic:
norm_cast at hq ⊢

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < q.num
⊢ 1 ≤ q.num - ↑q.den

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 0 ≤ 1 / ↑k

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ a ≤ ↑q

Tactic:
refine (ha q.den (by positivity)).trans ?_

Result:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 / ↑q.den + 1 ≤ ↑q

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ (1 / ↑k * ↑k + 1) ^ (2 * k) ≤ ((1 / ↑k + 1) ^ k) ^ (2 * k)

Tactic:
gcongr

Result:
case hab
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 1 / ↑k * ↑k + 1 ≤ (1 / ↑k + 1) ^ k

Proof state:
case hab
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 1 / ↑k * ↑k + 1 ≤ (1 / ↑k + 1) ^ k

Tactic:
exact mul_add_one_le_add_one_pow (by simp) _

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q.num / ↑q.den
⊢ 0 < ↑q.den

Tactic:
positivity

Result:
no goals

Proof state:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 0 < q.den

Tactic:
positivity

Result:
no goals

Proof state:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 ^ (2 * k) = (1 / ↑k * ↑k + 1) ^ (2 * k)

Tactic:
simp [posk.ne']

Result:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1