awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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₁
calc : ‖f m‖ = ‖f m‖ / ‖g m‖ * ‖g m‖
calc₁ : ‖f m‖ / ‖g m‖ * ‖g m‖ ≤ C₁ * ‖g m‖
⊢ ‖f m‖ ≤ C₁ * ‖g m‖

Tactic:
calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)

Premises used: Norm.norm, HDiv.hDiv
-- 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‖
⊢ C₁ ∈ ubounds

Tactic:
have C₁_mem : C₁ ∈ ubounds := by
    rw [Set.mem_setOf]
    intro m hm
    calc ‖f m‖ = (‖f m‖ / ‖g m‖) * ‖g m‖ := by by_cases hm' : g m = 0 <;> grind [norm_eq_zero]
      _ ≤ C₁ * ‖g m‖ := by
        gcongr
        exact Finset.le_sup' (fun x => ‖f x‖ / ‖g x‖) (Finset.mem_def.mpr hm)
-- 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‖
C₁_mem : C₁ ∈ ubounds
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
⟨max C₀ C₁, ?_⟩

Premises used: Max.max, Exists.intro
-- 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‖
C₁_mem : C₁ ∈ ubounds
refine : ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ max C₀ C₁ * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ c * ‖g x‖

Tactic:
refine ⟨max C₀ C₁, ?_⟩
-- 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‖
C₁_mem : C₁ ∈ ubounds
h₁ : ∀ (n : ℕ) (hn : n₁ ≤ n), ‖f n‖ ≤ max C₀ C₁ * ‖g n‖
⊢ ∀ᶠ (x : ℕ) in atTop, ‖f x‖ ≤ max C₀ C₁ * ‖g x‖

Tactic:
filter_upwards [eventually_ge_atTop n₁] with n hn

Premises used: 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ n₁ ≤ n

Tactic:
grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
⊢ max C₀ C₁ ≥ C₀

Tactic:
grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
h₁ : ∀ (m : ℕ) (hm : m ∈ Finset.Ico n₀ n), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖

Tactic:
refine H₂ _ (by grind) _ (by grind) fun m hm => ?_
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
pos : ∀ (hbase : m < n₁), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
neg : ∀ (hbase : ¬m < n₁), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
by_cases hbase : m < n₁
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
⊢ C₁ ≤ max C₀ C₁

Tactic:
grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
⊢ C₁ ≤ max C₀ C₁

Tactic:
have hC₁ : C₁ ≤ max C₀ C₁ := by grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
hC₁ : C₁ ≤ max C₀ C₁
pos : ‖f m‖ ≤ C₁ * ‖g m‖
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
grw [← hC₁]
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : m < n₁
hC₁ : C₁ ≤ max C₀ C₁
⊢ ‖f m‖ ≤ C₁ * ‖g m‖

Tactic:
grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖
hn : n₁ ≤ n
m : ℕ
hm : m ∈ Finset.Ico n₀ n
hbase : ¬m < n₁
⊢ ‖f m‖ ≤ max C₀ C₁ * ‖g m‖

Tactic:
grind
-- 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‖
C₁_mem : C₁ ∈ ubounds
n : ℕ
hn : n₁ ≤ n
h₁ : ∀ (n : ℕ) (h_ind : ∀ m < n, ∀ (hn : n₁ ≤ m), ‖f m‖ ≤ max C₀ C₁ * ‖g m‖) (hn : n₁ ≤ n), ‖f n‖ ≤ max C₀ C₁ * ‖g n‖
⊢ ‖f n‖ ≤ max C₀ C₁ * ‖g n‖

Tactic:
induction n using Nat.strongRecOn with
  | ind n h_ind =>
    refine H₂ _ (by grind) _ (by grind) fun m hm => ?_
    by_cases hbase : m < n₁
    · have hC₁ : C₁ ≤ max C₀ C₁ := by grind
      grw [← hC₁]
      grind
    · grind
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
⊢ f =O[atTop] g

Tactic:
isBigO_nat_atTop_induction ?hzero ?hrec

Premises used: Asymptotics.isBigO_nat_atTop_induction
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
refine : ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0
refine₁ :
  ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ (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

Tactic:
refine isBigO_nat_atTop_induction ?hzero ?hrec

Premises used: Asymptotics.isBigO_nat_atTop_induction
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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 : ∀ (a : ℕ), 0 ≤ f a → 0 < g a → g a = 0 → f a = 0
⊢ ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0

Tactic:
filter_upwards [hf, hg]
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
⊢ ∀ (a : ℕ), 0 ≤ f a → 0 < g a → g a = 0 → f a = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
⊢ ∀ᶠ (n : ℕ) in atTop, g n = 0 → f n = 0

Tactic:
case hzero => filter_upwards [hf, hg]; grind
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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 :
  ∀ (n₀ : ℕ) (hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y) (hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y)
    (hnrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∀ᶠ (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:
filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec

Premises used: Iff.mpr, Filter.eventually_forall_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
hnrec : ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (C₀ : ℝ) (hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n),
    ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
obtain ⟨C₀, hnrec⟩ := hnrec
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
⟨C₀, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
⊢ ∃ (C₀ : ℝ), ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
refine ⟨C₀, ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
h :
  ∀ (a : ℕ),
    (∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, f m ≤ C * g m) → f a ≤ C * g a) →
      n₀ ≤ a → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, ‖f m‖ ≤ C * ‖g m‖) → ‖f a‖ ≤ C * ‖g a‖
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
filter_upwards [hnrec, eventually_ge_atTop n₀]

Premises used: Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
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
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
C₀ : ℝ
hnrec : ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ (a : ℕ),
    (∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, f m ≤ C * g m) → f a ≤ C * g a) →
      n₀ ≤ a → ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ a, ‖f m‖ ≤ C * ‖g m‖) → ‖f a‖ ≤ C * ‖g a‖

Tactic:
grind [Real.norm_eq_abs]

Premises used: Real.norm_eq_abs
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
ι : Type u_1
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : f =O[cofinite] g
⊢ Summable f

Tactic:
let ⟨_, hC⟩ := h.isBigOWith
  .of_norm_bounded_eventually (hg.abs.mul_left _) hC.bound

Premises used: Summable.abs, Summable.mul_left, _private.0.summable_of_isBigO.match_1, Summable.of_norm_bounded_eventually, Asymptotics.IsBigO.isBigOWith, Summable, Asymptotics.IsBigOWith.bound, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Asymptotics.Lemmas
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → E
g : ℕ → ℝ
hg : Summable g
h : f =O[atTop] g
⊢ Summable f

Tactic:
summable_of_isBigO hg <| Nat.cofinite_eq_atTop.symm ▸ h

Premises used: Eq.rec, summable_of_isBigO, Nat.cofinite_eq_atTop, Eq.symm