Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: 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

pp: case inr
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:
· obtain rfl : f = 0 := by
        ext n
        simpa using H n
      simp only [lt_irrefl, false_or] at h₀
      exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩

Goal state after:
case inr
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