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

Tactic:
8

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
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
⊢ ∀ (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

Tactic:
2 → 8

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

Tactic:
⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩

Premises used: Filter.Eventually.mono, zero_lt_one, And.intro, Exists.intro, Asymptotics.IsLittleO.def
-- 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
refine : ∀ (n : ℕ) (hn : ‖f n‖ ≤ 1 * ‖a ^ n‖), |f n| ≤ a ^ n
⊢ ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n

Tactic:
refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
-- 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
a : ℝ
ha : a ∈ Set.Ioo 0 R
H : IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
n : ℕ
hn : ‖f n‖ ≤ 1 * ‖a ^ n‖
rwa : ∀ (hn : |f n| ≤ 1 * ‖a ^ n‖), |f n| ≤ a ^ n
rwa₁ : ∀ (hn : |f n| ≤ 1 * |a ^ n|), |f n| ≤ a ^ n
rwa₂ : ∀ (hn : |f n| ≤ |a ^ n|), |f n| ≤ a ^ n
rwa₃ : ∀ (hn : |f n| ≤ |a| ^ n), |f n| ≤ a ^ n
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (hn : |f n| ≤ a ^ n), |f n| ≤ a ^ n
⊢ |f n| ≤ a ^ n

Tactic:
rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn

Premises used: And.left, abs_of_pos, one_mul, 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
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
⊢ ∀ (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

Tactic:
tfae_have 2 → 8
  | ⟨a, ha, H⟩ => by
    refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
    rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
-- 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
⊢ ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n

Tactic:
8

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

Tactic:
7

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

Tactic:
8 → 7

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

Tactic:
tfae_have 8 → 7 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, 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 < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n

Tactic:
7

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
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 ∈ 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
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:
7 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false