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
a : ℝ
ha : a ∈ Set.Ioo (-R) R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
b : ℝ
hab : |a| < b
hbR : b < R
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
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)))⟩
-- 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
⊢ ∀ (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

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)))⟩
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
2 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
4 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
tfae_have 4 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, 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
⊢ ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
4 → 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
rcases :
  ∀ (C : ℝ) (hC₀ : C > 0) (hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩

Premises used: Asymptotics.bound_of_isBigO_nat_atTop
-- 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
⟨a, ha, C, hC₀, fun n ↦ ?_⟩

Premises used: 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
refine : ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
-- 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
C : ℝ
hC₀ : C > 0
hC : ∀ ⦃x : ℕ⦄, a ^ x ≠ 0 → ‖f x‖ ≤ C * ‖a ^ x‖
n : ℕ
⊢ |f n| ≤ C * a ^ n

Tactic:
simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')

Premises used: pow_ne_zero, LT.lt.le, LT.lt.ne', And.left, abs_of_nonneg, Real.norm_eq_abs, abs_pow
-- 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
⊢ ∀ (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

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')
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
6 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
tfae_have 6 → 5 := fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩