awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)

Tactic:
have hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1) := by
    rw [← Real.one_rpow r]
    exact Tendsto.comp (Real.continuousAt_rpow_const _ _ (by left; norm_num)) hφ
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
h₁ : u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
⊢ ∃ (φ : α → ℝ) (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r

Tactic:
use (· ^ r) ∘ φ, hφr

Premises used: HPow.hPow
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
enter : (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
| u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r

Tactic:
enter [3]
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
enter : fun (x : α) ↦ φ x ^ r * v x ^ r
| u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r

Tactic:
enter [3]; change fun x ↦ φ x ^ r * v x ^ r

Premises used: HMul.hMul, HPow.hPow
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
h₁ : ∀ (x : α) (hφ_pos : 0 < φ x) (huv' : u x = (φ * v) x), (u ^ r) x = φ x ^ r * v x ^ r
⊢ u ^ r =ᶠ[l] fun (x : α) ↦ φ x ^ r * v x ^ r

Tactic:
filter_upwards [Tendsto.eventually_const_lt (zero_lt_one) hφ, huφv] with x hφ_pos huv'

Premises used: Filter.Tendsto.eventually_const_lt, zero_lt_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
x : α
hφ_pos : 0 < φ x
huv' : u x = (φ * v) x
⊢ (u ^ r) x = φ x ^ r * v x ^ r

Tactic:
simp [← Real.mul_rpow (le_of_lt hφ_pos) (hv x), huv']

Premises used: le_of_lt, Real.mul_rpow
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
⊢ ∀ᶠ (x : α) in l, g x ≠ 0

Tactic:
have hg := g_tendsto.eventually_ne_atTop 0
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x ≠ 0

Tactic:
have hf := hfg.symm.tendsto_atTop g_tendsto |>.eventually_ne_atTop 0
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ Tendsto (f / g) l (𝓝 1)

Tactic:
rw [isEquivalent_iff_tendsto_one hg] at hfg

Premises used: Asymptotics.isEquivalent_iff_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
hfg₁ : Tendsto (f / g) l (𝓝 1)
⊢ Tendsto g l atTop

Tactic:
rw [isEquivalent_iff_tendsto_one hg] at hfg

Premises used: Asymptotics.isEquivalent_iff_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
hfg₁ : Tendsto (f / g) l (𝓝 1)
g_tendsto₁ : Tendsto g l atTop
⊢ ∀ᶠ (x : α) in l, g x ≠ 0

Tactic:
rw [isEquivalent_iff_tendsto_one hg] at hfg

Premises used: Asymptotics.isEquivalent_iff_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
hfg₁ : Tendsto (f / g) l (𝓝 1)
g_tendsto₁ : Tendsto g l atTop
hg₁ : ∀ᶠ (x : α) in l, g x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x ≠ 0

Tactic:
rw [isEquivalent_iff_tendsto_one hg] at hfg

Premises used: Asymptotics.isEquivalent_iff_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ Ne (α := ℝ) 1 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg_1 : ∀ᶠ (x : α) in l, g x ≠ 0
hf_1 : ∀ᶠ (x : α) in l, f x ≠ 0
n : α
hf : f n ≠ 0
hg : g n ≠ 0
⊢ Real.log ((f / g) n) = Real.log (f n) - Real.log (g n)

Tactic:
Real.log_div hf hg

Premises used: Real.log_div
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≠ 0) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≠ 0) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ (fun (x : α) ↦ Real.log ((f / g) x)) x = Real.log (f x) - Real.log (g x)) x}
                  x}
            x}
      a
h₁ h₂ : ∀ (n : α) (hf : f n ≠ 0) (hg : g n ≠ 0), Real.log ((f / g) n) = Real.log (f n) - Real.log (g n)
⊢ l.EventuallyEq (β := ℝ) (fun (x : α) ↦ Real.log ((f / g) x)) fun (n : α) ↦ Real.log (f n) - Real.log (g n)

Tactic:
filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ Tendsto (fun (n : α) ↦ Real.log (f n) - Real.log (g n)) l (𝓝 (Real.log 1))

Tactic:
have := hfg.log (by norm_num) |>.congr' <| by
    filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
this : Tendsto (fun (n : α) ↦ Real.log (f n) - Real.log (g n)) l (𝓝 (Real.log 1))
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (n : α) ↦ Real.log (f n) - Real.log (g n)) fun (x : α) ↦ 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
this : Tendsto (fun (n : α) ↦ Real.log (f n) - Real.log (g n)) l (𝓝 (Real.log 1))
⊢ IsEquivalent (E' := ℝ) l (fun (n : α) ↦ Real.log (f n)) fun (n : α) ↦ Real.log (g n)

Tactic:
exact IsLittleO.isEquivalent <| calc
    (fun n ↦ Real.log (f n) - Real.log (g n)) =o[l] fun _ ↦ (1 : ℝ) := by simpa
    _ =o[l] fun n ↦ Real.log (g n) := isLittleO_one_left_iff ℝ |>.mpr <|
      tendsto_norm_atTop_atTop.comp <| Real.tendsto_log_atTop.comp g_tendsto

Premises used: Iff.mpr, Real, HSub.hSub, Asymptotics.isLittleO_one_left_iff, Real.log, tendsto_norm_atTop_atTop, Real.tendsto_log_atTop, Filter.Tendsto.comp, OfNat.ofNat, Asymptotics.IsLittleO.isEquivalent
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
⊢ ∀ (i : ℕ), ‖g i‖ = g i

Tactic:
have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
rwa : Eq (α := ℝ) |∑ i ∈ range n, g i| (∑ i ∈ range n, g i)
rwa₁ : Eq (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range n, g i)
rwa₂ : ∀ (i : ℕ), 0 ≤ g i
rwa₃ : Eq (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range n, g i)
rwa₄ rwa₅ rwa₆ : ∀ (i : ℕ), 0 ≤ g i
⊢ norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i

Tactic:
rwa [Real.norm_eq_abs, abs_sum_of_nonneg']

Premises used: Finset.abs_sum_of_nonneg', Real.norm_eq_abs
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
⊢ ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i

Tactic:
have B : ∀ n, ‖∑ i ∈ range n, g i‖ = ∑ i ∈ range n, g i := fun n => by
    rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
apply :
  ∀ (ε : ℝ) (εpos : 0 < ε),
    ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i

Tactic:
apply isLittleO_iff.2 fun ε εpos => _

Premises used: Iff.mpr, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
⊢ ∃ (N : ℕ), ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b

Tactic:
simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)

Premises used: half_pos, Iff.mp, Asymptotics.isLittleO_iff, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
obtain :
  ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b),
    ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)
⊢ ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ b : ℕ, N ≤ b → ‖f b‖ ≤ ε / 2 * g b := by
    simpa only [A, eventually_atTop] using isLittleO_iff.mp h (half_pos εpos)
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
apply :
  Eq.{u_1 + 1} (α := α) (∑ i ∈ range N, f i) 0 ∨
    Tendsto (α := ℕ) (Function.comp (β := ℝ) norm fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i

Tactic:
apply isLittleO_const_left.2

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ Eq.{u_1 + 1} (α := α) (∑ i ∈ range N, f i) 0 ∨
    Tendsto (α := ℕ) (Function.comp (β := ℝ) norm fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop

Tactic:
Or.inr (h'g.congr fun n => (B n).symm)

Premises used: Filter.Tendsto.congr, Eq.symm, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ Eq.{u_1 + 1} (α := α) (∑ i ∈ range N, f i) 0 ∨
    Tendsto (α := ℕ) (Function.comp (β := ℝ) norm fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop

Tactic:
exact Or.inr (h'g.congr fun n => (B n).symm)

Premises used: Filter.Tendsto.congr, Eq.symm, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i

Tactic:
have : (fun _ : ℕ => ∑ i ∈ range N, f i) =o[atTop] fun n : ℕ => ∑ i ∈ range n, g i := by
    apply isLittleO_const_left.2
    exact Or.inr (h'g.congr fun n => (B n).symm)
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
h₁ :
  ∀ (n : ℕ) (hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i))
    (Nn : n ∈ Set.Ici N), norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)
⊢ ∀ᶠ (x : ℕ) in atTop, norm.{u_1} (E := α) (∑ i ∈ range x, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range x, g i)

Tactic:
filter_upwards [isLittleO_iff.1 this (half_pos εpos), Ici_mem_atTop N] with n hn Nn

Premises used: half_pos, Filter.Ici_mem_atTop, Iff.mp, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
rw rw₁ : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = norm.{u_1} (E := α) (∑ k ∈ range n, f k)
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖

Tactic:
rw [sum_range_add_sum_Ico _ Nn]

Premises used: Finset.sum_range_add_sum_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖ ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + norm.{u_1} (E := α) (∑ i ∈ Ico N n, f i)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + norm.{u_1} (E := α) (∑ i ∈ Ico N n, f i) ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i

Tactic:
(add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))

Premises used: le_rfl, add_le_add, norm_sum_le_of_le, And.left, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
bc : ∀ i ∈ range n, i ∉ Ico N n → 0 ≤ ε / 2 * g i
bc₁ : Ico N n ⊆ range n
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, ε / 2 * g i ≤
    norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ ∀ i ∈ range n, i ∉ Ico N n → 0 ≤ ε / 2 * g i

Tactic:
fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)

Premises used: mul_nonneg, half_pos, LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ ∀ i ∈ range n, i ∉ Ico N n → 0 ≤ ε / 2 * g i

Tactic:
exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)

Premises used: mul_nonneg, half_pos, LT.lt.le
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
bc : Ico N n ⊆ Ico 0 n
⊢ Ico N n ⊆ range n

Tactic:
rw [range_eq_Ico]

Premises used: Finset.range_eq_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n

Tactic:
Ico_subset_Ico zero_le le_rfl

Premises used: zero_le, le_rfl, Finset.Ico_subset_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ Ico N n ⊆ Ico 0 n

Tactic:
exact Ico_subset_Ico zero_le le_rfl

Premises used: zero_le, le_rfl, Finset.Ico_subset_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
rw :
  norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ε / 2 * ∑ i ∈ range n, g i ≤
    ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ∑ i ∈ range n, ε / 2 * g i ≤
    ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i

Tactic:
rw [← mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (x : ℕ) ↦ ∑ i ∈ range N, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
n : ℕ
hn : norm.{u_1} (E := α) (∑ i ∈ range N, f i) ≤ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i)
Nn : n ∈ Set.Ici N
⊢ norm.{u_1} (E := α) (∑ i ∈ range N, f i) + ε / 2 * ∑ i ∈ range n, g i ≤
    ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i

Tactic:
gcongr