-- 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 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 < g y) x} x →
          Membership.mem (γ := Set ℕ)
            {x : ℕ |
              Membership.mem (γ := Set ℕ) {x : ℕ | (fun (x : ℕ) ↦ ∀ (y : ℕ), x ≤ y → 0 ≤ f y) x} x →
                Membership.mem (γ := Set ℕ)
                  {x : ℕ |
                    Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n)
                            x}
                        x →
                      Membership.mem (γ := Set ℕ)
                        {x : ℕ |
                          (fun (n₀ : ℕ) ↦
                              ∃ (C₀ : ℝ),
                                ∀ᶠ (n : ℕ) in atTop,
                                  ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖)
                            x}
                        x}
                  x}
            x}
      a
h₁ 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‖
h₃ :
  ∀ (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‖
h₄ :
  ∀ (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),
    ∀ᶠ (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) (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‖
⊢ ∀ᶠ (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:
case hrec =>
    filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec
    obtain ⟨C₀, hnrec⟩ := hnrec
    refine ⟨C₀, ?_⟩
    filter_upwards [hnrec, eventually_ge_atTop n₀]
    grind [Real.norm_eq_abs]

Premises used: Iff.mpr, Filter.eventually_forall_ge_atTop, Real.norm_eq_abs