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

Tactic:
5 → 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
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
inl :
  ∀ (h₀ : LT.lt (α := ℝ) 0 0 ∨ 0 < R) (H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
inr : ∀ (hC₀ : 0 < C) (ha₀ : 0 ≤ a), ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)

Premises used: LE.le.trans, sign_cases_of_C_mul_pow_nonneg, abs_nonneg, rfl
-- 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
a : ℝ
ha : a < R
h₀ : LT.lt (α := ℝ) 0 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
h : ∀ (n : ℕ), f n = 0 n
⊢ f = 0

Tactic:
ext 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
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
a : ℝ
ha : a < R
h₀ : LT.lt (α := ℝ) 0 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
n : ℕ
⊢ f n = 0 n

Tactic:
simpa using H 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
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
a : ℝ
ha : a < R
h₀ : LT.lt (α := ℝ) 0 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
inl :
  ∀
    (tfae_1_to_3 :
      ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x)
    (tfae_2_to_1 :
      ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x)
    (tfae_3_to_2 :
      ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x)
    (tfae_2_to_4 :
      ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x)
    (tfae_4_to_3 :
      ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x)
    (tfae_4_to_6 :
      ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
        ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n)
    (tfae_6_to_5 :
      ∀ (a : ∃ 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, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

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

Premises used: rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
h₀ : LT.lt (α := ℝ) 0 0 ∨ 0 < R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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
⊢ 0 < R

Tactic:
simp only [lt_irrefl, false_or] at h₀

Premises used: lt_irrefl, false_or
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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
h₀ : 0 < R
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x

Tactic:
⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩

Premises used: Iff.mpr, Asymptotics.isBigO_zero, neg_lt_zero, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
a : ℝ
ha : a < R
tfae_1_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_1 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_3_to_2 :
  ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_2_to_4 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsLittleO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_3 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x
tfae_4_to_6 :
  ∀ (a : ∃ a ∈ Set.Ioo 0 R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x),
    ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |0 n| ≤ C * a ^ n
tfae_6_to_5 :
  ∀ (a : ∃ 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
h₀ : 0 < R
⊢ ∃ a ∈ Set.Ioo (-R) R, IsBigO (E := ℝ) (F := ℝ) atTop 0 fun (x : ℕ) ↦ a ^ x

Tactic:
exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
-- 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
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, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩

Premises used: le_abs_self, LT.lt.le, Asymptotics.isBigO_of_le', HPow.hPow, And.intro, Exists.intro, LE.le.trans, mul_le_mul_of_nonneg_left
-- 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
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, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x

Tactic:
exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
-- 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
⊢ ∀ (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

Tactic:
tfae_have 5 → 3
  | ⟨a, ha, C, h₀, H⟩ => by
    rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
    · 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 _ _⟩
    exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
-- 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, 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