awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ 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
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ 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
refine : 0 ≤ a
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
refine ⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ 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:
nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)

Premises used: Filter.nonneg_of_eventually_pow_nonneg, Filter.Eventually.mono, LE.le.trans, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ 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)

Premises used: Filter.nonneg_of_eventually_pow_nonneg, Filter.Eventually.mono, LE.le.trans, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n), ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
⊢ ∀ (a : ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n), ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
tfae_have 7 → 3
  | ⟨a, ha, H⟩ => by
    refine ⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩
    exact nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
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 : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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 : ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
tfae_2_to_8 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n
tfae_8_to_7 : ∀ (a : ∃ 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 : ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n), ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ [∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f 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
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)

Tactic:
have : Tendsto (fun x : ℝ ↦ x ^ k) (𝓝[>] 1) (𝓝 1) :=
    ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
obtain :
  ∀ (r' : ℝ) (hr' : r' ^ k < r) (h1 : 1 < r'),
    IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ r ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ r ^ n

Tactic:
obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ :=
    ((this.eventually (gt_mem_nhds hr)).and self_mem_nhdsWithin).exists

Premises used: gt_mem_nhds, Filter.Eventually.and, Filter.Eventually.exists, self_mem_nhdsWithin, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
⊢ 0 ≤ r'

Tactic:
have h0 : 0 ≤ r' := zero_le_one.trans h1.le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
suffices :
  IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ k) ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ r ^ n

Tactic:
suffices (fun n ↦ (n : R) ^ k : ℕ → R) =O[atTop] fun n : ℕ ↦ (r' ^ k) ^ n from
    this.trans_isLittleO (isLittleO_pow_pow_of_lt_left (pow_nonneg h0 _) hr')
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
rw : (r' ^ n) ^ k
| (r' ^ k) ^ n

Tactic:
rw [← pow_mul, mul_comm, pow_mul]

Premises used: pow_mul, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
conv :
  IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ n) ^ k
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ k) ^ n

Tactic:
conv in (r' ^ _) ^ _ => rw [← pow_mul, mul_comm, pow_mul]

Premises used: pow_mul, HPow.hPow, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
suffices : ∀ (n : ℕ), norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * norm.{u_2} (E := R) 1 * ‖r' ^ n‖
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦ (r' ^ n) ^ k

Tactic:
suffices ∀ n : ℕ, ‖(n : R)‖ ≤ (r' - 1)⁻¹ * ‖(1 : R)‖ * ‖r' ^ n‖ from
    (isBigO_of_le' _ this).pow _
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
rw : norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * norm.{u_2} (E := R) 1
⊢ norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * norm.{u_2} (E := R) 1 * ‖r' ^ n‖

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * norm.{u_2} (E := R) 1

Tactic:
n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))

Premises used: mul_le_mul_of_nonneg_right, Nat.norm_cast_le, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
refine : (↑n : ℝ) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖
⊢ norm.{u_2} (E := R) (↑n : R) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖ * norm.{u_2} (E := R) 1

Tactic:
refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))

Premises used: mul_le_mul_of_nonneg_right, Nat.norm_cast_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r : ℝ
hr : 1 < r
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ k) (𝓝[>] 1) (𝓝 1)
r' : ℝ
hr' : r' ^ k < r
h1 : 1 < r'
h0 : 0 ≤ r'
n : ℕ
⊢ (↑n : ℝ) ≤ (r' - 1)⁻¹ * ‖r' ^ n‖

Tactic:
simpa [_root_.div_eq_inv_mul, Real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1

Premises used: abs_of_nonneg, div_eq_inv_mul, Nat.cast_le_pow_div_sub, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
r : ℝ
hr : 1 < r
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ r ^ n

Tactic:
simpa only [pow_one] using @isLittleO_pow_const_const_pow_of_one_lt R _ 1 _ hr

Premises used: pow_one, OfNat.ofNat, isLittleO_pow_const_const_pow_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
pos :
  ∀ (h0 : r₁ = 0),
    IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
      r₂ ^ n
neg :
  ∀ (h0 : ¬r₁ = 0),
    IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
      r₂ ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n

Tactic:
by_cases h0 : r₁ = 0
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n

Tactic:
(isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl

Premises used: Iff.mpr, Filter.mem_atTop_sets, Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr', Exists.intro, Filter.EventuallyEq.rfl, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
pos :
  ∀ (n : ℕ) (hn : n ≥ 1),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        (fun (x : ℕ) ↦
            Eq.{u_2 + 1} (α := R) ((fun (_x : ℕ) ↦ (0 : R)) x)
              ((fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) x))
          x}
      n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n

Tactic:
refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl

Premises used: Iff.mpr, Filter.mem_atTop_sets, Asymptotics.isLittleO_zero, Asymptotics.IsLittleO.congr', Exists.intro, Filter.EventuallyEq.rfl, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ Membership.mem (γ := Set ℕ)
    {x : ℕ |
      (fun (x : ℕ) ↦
          Eq.{u_2 + 1} (α := R) ((fun (_x : ℕ) ↦ (0 : R)) x) ((fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) x))
        x}
    n

Tactic:
simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]

Premises used: Iff.mp, Nat.one_le_iff_ne_zero, zero_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ 0 < ‖r₁‖

Tactic:
rw [← Ne, ← norm_pos_iff] at h0

Premises used: norm_pos_iff, Ne
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n

Tactic:
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
    isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A :
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n
this : IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ ‖r₁‖ ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n

Tactic:
simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this

Premises used: pow_pos, div_mul_cancel₀, LT.lt.ne', div_pow, Asymptotics.IsLittleO.mul_isBigO
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A :
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n
neg : IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ ‖r₁‖ ^ n
⊢ IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k * r₁ ^ n) fun (n : ℕ) ↦
    r₂ ^ n

Tactic:
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
    simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A :
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ ‖r₁‖ ^ n

Tactic:
.of_norm_eventuallyLE <| eventually_norm_pow_le r₁

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE, eventually_norm_pow_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : Type u_2
inst : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A :
  IsLittleO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ HPow.hPow (α := R) (↑n : R) k) fun (n : ℕ) ↦
    (r₂ / ‖r₁‖) ^ n
⊢ IsBigO.{0, u_2, 0} (E := R) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ ‖r₁‖ ^ n

Tactic:
exact .of_norm_eventuallyLE <| eventually_norm_pow_le r₁

Premises used: eventually_norm_pow_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : 1 < r
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k / r ^ n) atTop (𝓝 0)

Tactic:
(isLittleO_pow_const_const_pow_of_one_lt k hr).tendsto_div_nhds_zero

Premises used: Asymptotics.IsLittleO.tendsto_div_nhds_zero, isLittleO_pow_const_const_pow_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
pos : ∀ (h0 : r = 0), Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
neg : ∀ (h0 : ¬r = 0), Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)

Tactic:
by_cases h0 : r = 0
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
n : ℕ
hn : n ≥ 1
⊢ Membership.mem (γ := Set ℕ)
    {x : ℕ | (fun (x : ℕ) ↦ Eq (α := ℝ) 0 ((fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) x)) x} n

Tactic:
simp [zero_lt_one.trans_le hn |>.ne', h0]

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
k : ℕ
r : ℝ
hr : |r| < 1
h0 : r = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) k * r ^ n) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds.congr'
      (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn |>.ne', h0]⟩)

Premises used: Iff.mpr, tendsto_const_nhds, Filter.mem_atTop_sets, Exists.intro, Filter.Tendsto.congr', OfNat.ofNat