-- 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
tfae_7_to_3 : (∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n) → ∃ 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_finish

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
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
⊢ [∃ 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 4 → 6
| ⟨a, ha, H⟩ => by
  rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
  refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
  simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')

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
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
⊢ [∃ 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

Proof state:
case inl
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
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x => a ^ x

Tactic:
obtain rfl : f = 0 := by
  ext n
  simpa using H n

Result:
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
h₀ : 0 < 0 ∨ 0 < 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
⊢ ∃ a ∈ Set.Ioo (-R) R, 0 =O[atTop] fun x => a ^ x