-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
    TFAE
      [∃ a ∈ Ioo (-R) R, f =o[atTop] (a ^ ·), ∃ a ∈ Ioo 0 R, f =o[atTop] (a ^ ·),
        ∃ a ∈ Ioo (-R) R, f =O[atTop] (a ^ ·), ∃ a ∈ Ioo 0 R, f =O[atTop] (a ^ ·),
        ∃ a < R, ∃ C : ℝ, (0 < C ∨ 0 < R) ∧ ∀ n, |f n| ≤ C * a ^ n,
        ∃ a ∈ Ioo 0 R, ∃ C > 0, ∀ n, |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ n in atTop, |f n| ≤ a ^ n,
        ∃ a ∈ Ioo 0 R, ∀ᶠ n in atTop, |f n| ≤ a ^ n]

Proof state:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_5_to_3 :
  (∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_2_to_8 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : (∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
a : ℝ
ha : a < R
H : ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ 0 ≤ a

Tactic:
exact nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)

Result:
no goals

Proof state:
case inr.intro
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
hC₀ : 0 < C
ha₀ : 0 ≤ a
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x

Tactic:
exact ⟨a, A ⟨ha₀, ha⟩,
  isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩

Result:
no goals

Proof state:
case inl
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x => a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, 0 =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x => a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x => a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, 0 =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |0 n| ≤ C * a ^ n
H : ∀ (n : ℕ), |0 n| ≤ 0 * a ^ n
h₀ : 0 < R
⊢ ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x => a ^ x

Tactic:
exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩

Result:
no goals

Proof state:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE

Tactic:
tfae_have 3 → 2
| ⟨a, ha, H⟩ => by
  rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
  exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
    H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩

Result:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x
⊢ [∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x => a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x => a ^ x,
      ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE