awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
C : ℝ
hC : 0 ≤ C
this : ∀ (x : α), 0 ≤ C * ‖g' x‖
⊢ IsBigOWith C l f g' ↔ ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) C l (fun (x : α) ↦ f x i) g'

Tactic:
simp only [isBigOWith_iff, pi_norm_le_iff_of_nonneg (this _), eventually_all]

Premises used: pi_norm_le_iff_of_nonneg, Filter.eventually_all, Asymptotics.isBigOWith_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
simp :
  (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔
    ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) x l (fun (x : α) ↦ f x i) g'
⊢ f =O[l] g' ↔ ∀ (i : ι), IsBigO.{u_1, u_18, u_7} (E := E' i) l (fun (x : α) ↦ f x i) g'

Tactic:
simp only [isBigO_iff_eventually_isBigOWith, ← eventually_all]

Premises used: Filter.eventually_all, Asymptotics.isBigO_iff_eventually_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔
    ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) x l (fun (x : α) ↦ f x i) g'

Tactic:
eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

Premises used: Iff.mpr, Asymptotics.isBigOWith_pi, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ᶠ (c : ℝ) in atTop, IsBigOWith c l f g') ↔
    ∀ᶠ (x : ℝ) in atTop, ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) x l (fun (x : α) ↦ f x i) g'

Tactic:
exact eventually_congr (eventually_atTop.2 ⟨0, fun c => isBigOWith_pi⟩)

Premises used: Iff.mpr, Asymptotics.isBigOWith_pi, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
simp :
  (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g'
⊢ f =o[l] g' ↔ ∀ (i : ι), IsLittleO.{u_1, u_18, u_7} (E := E' i) l (fun (x : α) ↦ f x i) g'

Tactic:
simp +contextual only [IsLittleO_def, isBigOWith_pi, le_of_lt]

Premises used: Asymptotics.isBigOWith_pi, le_of_lt, Asymptotics.IsLittleO_def
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g'

Tactic:
⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
F' : Type u_7
inst : SeminormedAddCommGroup F'
g' : α → F'
l : Filter α
ι : Type u_17
inst_1 : Fintype ι
E' : ι → Type u_18
inst_2 : (i : ι) → SeminormedAddCommGroup (E' i)
f : α → (i : ι) → E' i
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ (i : ι), IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g') ↔
    ∀ (i : ι) ⦃c : ℝ⦄, 0 < c → IsBigOWith.{u_1, u_18, u_7} (E := E' i) c l (fun (x : α) ↦ f x i) g'

Tactic:
exact ⟨fun h i c hc => h hc i, fun h c hc i => h i hc⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
R : Type u_17
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Archimedean R
f : R → E
g : R → F
h : f =O[atTop] g
⊢ IsBigO.{0, u_3, u_4} (E := E) (F := F) atTop (fun (n : ℕ) ↦ f (↑n : R)) fun (n : ℕ) ↦ g (↑n : R)

Tactic:
IsBigO.comp_tendsto h tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
R : Type u_17
inst_2 : Semiring R
inst_3 : PartialOrder R
inst_4 : IsStrictOrderedRing R
inst_5 : Archimedean R
f : R → E
g : R → F
h : f =o[atTop] g
⊢ IsLittleO.{0, u_3, u_4} (E := E) (F := F) atTop (fun (n : ℕ) ↦ f (↑n : R)) fun (n : ℕ) ↦ g (↑n : R)

Tactic:
IsLittleO.comp_tendsto h tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → E
g : α → F
rw : (∃ (c : ℝ), ∀ᶠ (x : α) in atTop, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
rw₁ rw₂ :
  (∀ᶠ (a₀ : α) in atTop, ∃ (b : ℝ), ∀ a ≥ a₀, ‖f a‖ ≤ b * ‖g a‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ), ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
rw [isBigO_iff, exists_eventually_atTop]

Premises used: Filter.exists_eventually_atTop, Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
G : Type u_5
G' : Type u_8
inst : Norm G
inst_1 : SeminormedAddCommGroup G'
α : Type u_17
inst_2 : SemilatticeSup α
inst_3 : Nonempty α
f : α → G
g : α → G'
simp_rw : (∃ c > 0, ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
simp_rw₁ :
  (∃ (c : ℝ) (_ : c > 0), ∀ᶠ (x : α) in atTop, c * ‖f x‖ ≤ ‖g x‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ (c : ℝ) (_ : c > 0), ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
simp_rw₂ :
  (∃ (x : { a : ℝ // a > 0 }), ∀ᶠ (x_1 : α) in atTop, (↑x : ℝ) * ‖f x_1‖ ≤ ‖g x_1‖) ↔
    ∀ᶠ (n₀ : α) in atTop, ∃ (x : { a : ℝ // a > 0 }), ∀ n ≥ n₀, (↑x : ℝ) * ‖f n‖ ≤ ‖g n‖
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖

Tactic:
simp_rw [isBigO_iff'', ← exists_prop, Subtype.exists', exists_eventually_atTop]

Premises used: Filter.exists_eventually_atTop, Subtype.exists', exists_prop, Asymptotics.isBigO_iff''
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
rw : (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
⊢ IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h ↔ IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x

Tactic:
rw [isBigOWith_iff, isBigOWith_iff]

Premises used: Asymptotics.isBigOWith_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
refine_1 : ∀ (h_1 : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖), ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖
refine_2 : ∀ (h_1 : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖), ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖
⊢ (∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h x‖) ↔ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h x / f x‖

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖

Tactic:
h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Eventually.congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
refine_1 : ∀ (x : α) (hx : f x ≠ 0), ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖

Tactic:
refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Eventually.congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖
x : α
hx : f x ≠ 0
refine_1 : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖
refine_1₁ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖)
refine_1₂ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖
refine_1₃ refine_1₄ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
⊢ ‖f x * g x‖ ≤ c * ‖h_1 x‖ ↔ ‖g x‖ ≤ c * ‖h_1 x / f x‖

Tactic:
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

Premises used: Iff.mpr, norm_pos_iff, le_div_iff₀', mul_div_assoc, norm_mul, norm_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖

Tactic:
h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Eventually.congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
refine_2 : ∀ (x : α) (hx : f x ≠ 0), ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h_1 x‖

Tactic:
refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_

Premises used: Filter.Eventually.of_forall, Filter.Eventually.mp, Filter.Eventually.congr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h_1 : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h_1 x / f x‖
x : α
hx : f x ≠ 0
refine_2 : ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₁ : ‖g x‖ ≤ c * (‖h_1 x‖ / ‖f x‖) ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₂ : ‖g x‖ ≤ c * ‖h_1 x‖ / ‖f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
refine_2₃ refine_2₄ : ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h_1 x‖
⊢ ‖g x‖ ≤ c * ‖h_1 x / f x‖ ↔ ‖f x * g x‖ ≤ c * ‖h_1 x‖

Tactic:
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

Premises used: Iff.mpr, norm_pos_iff, le_div_iff₀', mul_div_assoc, norm_mul, norm_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
rw :
  (∃ (c : ℝ), IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
    ∃ (c : ℝ), IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x
⊢ IsBigO (E := 𝕜) l (fun (x : α) ↦ f x * g x) h ↔ IsBigO (F := 𝕜) l g fun (x : α) ↦ h x / f x

Tactic:
rw [isBigO_iff_isBigOWith, isBigO_iff_isBigOWith]

Premises used: Asymptotics.isBigO_iff_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ (c : ℝ), IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
    ∃ (c : ℝ), IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x

Tactic:
simp [isBigOWith_mul_iff_isBigOWith_div hf]

Premises used: Asymptotics.isBigOWith_mul_iff_isBigOWith_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
rw :
  (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x
⊢ IsLittleO (E := 𝕜) l (fun (x : α) ↦ f x * g x) h ↔ IsLittleO (F := 𝕜) l g fun (x : α) ↦ h x / f x

Tactic:
rw [isLittleO_iff_forall_isBigOWith, isLittleO_iff_forall_isBigOWith]

Premises used: Asymptotics.isLittleO_iff_forall_isBigOWith
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
α : Type u_1
𝕜 : Type u_15
inst : NormedDivisionRing 𝕜
l : Filter α
f g h : α → 𝕜
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (E := 𝕜) c l (fun (x : α) ↦ f x * g x) h) ↔
    ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith (F := 𝕜) c l g fun (x : α) ↦ h x / f x

Tactic:
simp [isBigOWith_mul_iff_isBigOWith_div hf]

Premises used: Asymptotics.isBigOWith_mul_iff_isBigOWith_div
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0

Tactic:
rw [← eventually_forall_ge_atTop] at h

Premises used: Filter.eventually_forall_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
h₁ : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
rw [← eventually_forall_ge_atTop] at h

Premises used: Filter.eventually_forall_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
obtain :
  ∀ (n₀ : ℕ) (h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0)
    (hrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖),
    f =O[atTop] g
⊢ f =O[atTop] g

Tactic:
obtain ⟨n₀, h, hrec⟩ := h.and hrec |>.exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
hrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
obtain :
  ∀ (C₀ : ℝ) (hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖),
    f =O[atTop] g
⊢ f =O[atTop] g

Tactic:
obtain ⟨C₀, hrec⟩ := hrec
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
rw : ∃ (c : ℝ), ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[atTop] g

Tactic:
rw [isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖

Tactic:
rw [← eventually_forall_ge_atTop] at hrec

Premises used: Filter.eventually_forall_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
obtain :
  ∀ (n₁ : ℕ) (H₁ : n₀ ≤ n₁)
    (H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖),
    ∃ (c : ℝ), ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨n₁, H₁, H₂⟩ := (eventually_ge_atTop n₀).and hrec |>.exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
rw : ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C₁ * ‖g m‖
⊢ C₁ ∈ ubounds

Tactic:
rw [Set.mem_setOf]

Premises used: Set.mem_setOf
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
pos : ∀ (hm' : g m = 0), ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖
neg : ∀ (hm' : ¬g m = 0), ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖
⊢ ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖

Tactic:
by_cases hm' : g m = 0
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
hm' : g m = 0
⊢ ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖

Tactic:
grind [norm_eq_zero]

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
hm' : ¬g m = 0
⊢ ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖

Tactic:
grind [norm_eq_zero]

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
hbc : ‖f m‖ / ‖g m‖ ≤ C₁
⊢ ‖f m‖ / ‖g m‖ * ‖g m‖ ≤ C₁ * ‖g m‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E'' : Type u_9
F'' : Type u_10
inst : NormedAddCommGroup E''
inst_1 : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
h_1 : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → g y = 0 → f y = 0
hrec_1 :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
n₀ : ℕ
h : ∀ (y : ℕ), n₀ ≤ y → g y = 0 → f y = 0
C₀ : ℝ
hrec : ∀ᶠ (x : ℕ) in atTop, ∀ (y : ℕ), x ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
n₁ : ℕ
H₁ : n₀ ≤ n₁
H₂ : ∀ (y : ℕ), n₁ ≤ y → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ y, ‖f m‖ ≤ C * ‖g m‖) → ‖f y‖ ≤ C * ‖g y‖
ubounds : Set ℝ := {C : ℝ | ∀ m ∈ Finset.Icc n₀ n₁, ‖f m‖ ≤ C * ‖g m‖}
C₁ : ℝ := (Finset.Icc n₀ n₁).sup' ⋯ fun (n : ℕ) ↦ ‖f n‖ / ‖g n‖
m : ℕ
hm : m ∈ Finset.Icc n₀ n₁
⊢ ‖f m‖ / ‖g m‖ ≤ C₁

Tactic:
Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)

Premises used: Iff.mpr, Norm.norm, HDiv.hDiv, Finset.le_sup', Finset.mem_def