awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp : ε / 2 * ∑ i ∈ range n, g i + ε / 2 * ∑ i ∈ range n, g i = ε * ∑ i ∈ range n, g i
⊢ ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i = ε * norm (E := ℝ) (∑ i ∈ range n, g i)

Tactic:
simp only [B]
-- 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
⊢ ε / 2 * ∑ i ∈ range n, g i + ε / 2 * ∑ i ∈ range n, g i = ε * ∑ i ∈ range n, g i

Tactic:
ring
-- 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 : norm.{u_1} (E := α) (∑ i ∈ range n, f i) = ‖HAdd.hAdd (α := α) (∑ i ∈ range N, f i) (∑ i ∈ Ico N n, f i)‖
i₁ :
  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
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
i₃ : ε / 2 * norm (E := ℝ) (∑ i ∈ range n, g i) + ε / 2 * ∑ i ∈ range n, g i = ε * norm (E := ℝ) (∑ i ∈ range n, g i)
⊢ norm.{u_1} (E := α) (∑ i ∈ range n, f i) ≤ ε * norm (E := ℝ) (∑ i ∈ range n, g i)

Tactic:
calc
    ‖∑ i ∈ range n, f i‖ = ‖(∑ i ∈ range N, f i) + ∑ i ∈ Ico N n, f i‖ := by
      rw [sum_range_add_sum_Ico _ Nn]
    _ ≤ ‖∑ i ∈ range N, f i‖ + ‖∑ i ∈ Ico N n, f i‖ := norm_add_le _ _
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ Ico N n, ε / 2 * g i :=
      (add_le_add le_rfl (norm_sum_le_of_le _ fun i hi => hN _ (mem_Ico.1 hi).1))
    _ ≤ ‖∑ i ∈ range N, f i‖ + ∑ i ∈ range n, ε / 2 * g i := by
      gcongr
      · exact fun i _ _ ↦ mul_nonneg (half_pos εpos).le (hg i)
      · rw [range_eq_Ico]
        exact Ico_subset_Ico zero_le le_rfl
    _ ≤ ε / 2 * ‖∑ i ∈ range n, g i‖ + ε / 2 * ∑ i ∈ range n, g i := by rw [← mul_sum]; gcongr
    _ = ε * ‖∑ i ∈ range n, g i‖ := by
      simp only [B]
      ring

Premises used: le_rfl, add_le_add, norm_add_le, Finset.Ico, norm_sum_le_of_le, Finset.range, And.left, Iff.mp, Finset.sum, Finset.mem_Ico
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, 1) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, 1

Tactic:
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, 1) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, 1
⊢ ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ)) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
simp only [sum_const, card_range, Nat.smul_one_eq_cast] at this

Premises used: Finset.card_range, Nat.smul_one_eq_cast, Finset.sum_const
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ)) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
this tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  ∀ (h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑n : ℝ)) atTop atTop),
    IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
exact this tendsto_natCast_atTop_atTop

Premises used: tendsto_natCast_atTop_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
rw :
  IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1
⊢ Tendsto (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i)) atTop (𝓝 l)

Tactic:
rw [← tendsto_sub_nhds_zero_iff, ← isLittleO_one_iff ℝ]

Premises used: Real, Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)

Tactic:
have := Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 h)
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
apply :
  EventuallyEq.{0, u_1} (β := E) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, (u i - l))) fun (x : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l
apply₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (↑x : ℝ)) fun (_x : ℕ) ↦ 1
⊢ IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l) fun (_x : ℕ) ↦ 1

Tactic:
apply ((isBigO_refl (fun n : ℕ => (n : ℝ)⁻¹) atTop).smul_isLittleO this).congr' _ _

Premises used: Nat.cast, Asymptotics.IsLittleO.congr', Filter.atTop, Inv.inv, Asymptotics.IsBigO.smul_isLittleO, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
h₁ :
  ∀ (n : ℕ) (npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n),
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, (u i - l)) =
      HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i) - l
⊢ EventuallyEq.{0, u_1} (β := E) atTop
    (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, (u i - l))) fun (x : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := E) (↑x : ℝ)⁻¹ (∑ i ∈ range x, u i) - l

Tactic:
filter_upwards [Ici_mem_atTop 1] with n npos

Premises used: Filter.Ici_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have nposℝ : (0 : ℝ) < n := Nat.cast_pos.2 npos
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, (u i - l)) =
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i) - l

Tactic:
simp only [smul_sub, sum_sub_distrib, sum_const, card_range, sub_right_inj]

Premises used: sub_right_inj, Finset.card_range, smul_sub, Finset.sum_sub_distrib, Finset.sum_const
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (HSMul.hSMul (α := ℝ) (↑n : ℝ) l) = l
h₂ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) • l = l
h₃ : HSMul.hSMul (α := ℝ) 1 l = l
h₄ h₅ : l = l
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (n • l) = l

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul, inv_mul_cancel₀ nposℝ.ne', one_smul]

Premises used: Real, smul_smul, one_smul, LT.lt.ne', Nat.cast_smul_eq_nsmul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
h₁ : ∀ (n : ℕ) (npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n), HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := ℝ) (↑x : ℝ)⁻¹ (↑x : ℝ)) fun (_x : ℕ) ↦ 1

Tactic:
filter_upwards [Ici_mem_atTop 1] with n npos

Premises used: Filter.Ici_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : IsLittleO.{0, u_1, 0} (E := E) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, (u i - l)) fun (n : ℕ) ↦ (↑n : ℝ)
n : ℕ
npos : Membership.mem (γ := Set ℕ) (Set.Ici 1) n
nposℝ : LT.lt (α := ℝ) 0 (↑n : ℝ)
h₁ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1
h₂ h₃ : Eq (α := ℝ) 1 1
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) = 1

Tactic:
rw [smul_eq_mul, inv_mul_cancel₀ nposℝ.ne']

Premises used: LT.lt.ne', smul_eq_mul, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
u : ℕ → ℝ
l : ℝ
h : Tendsto u atTop (𝓝 l)
⊢ Tendsto (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (∑ i ∈ range n, u i)) atTop (𝓝 l)

Tactic:
h.cesaro_smul

Premises used: Filter.Tendsto.cesaro_smul
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedField R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : OrderTopology R
inst_4 : FloorRing R
⊢ IsEquivalent (E' := R) atTop (fun (x : R) ↦ (↑⌊x⌋₊ : R)) fun (x : R) ↦ x

Tactic:
isEquivalent_of_tendsto_one tendsto_nat_floor_div_atTop

Premises used: tendsto_nat_floor_div_atTop, Asymptotics.isEquivalent_of_tendsto_one
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedField R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : OrderTopology R
inst_4 : FloorRing R
⊢ IsEquivalent (E' := R) atTop (fun (x : R) ↦ (↑⌈x⌉₊ : R)) fun (x : R) ↦ x

Tactic:
isEquivalent_of_tendsto_one tendsto_nat_ceil_div_atTop

Premises used: Asymptotics.isEquivalent_of_tendsto_one, tendsto_nat_ceil_div_atTop
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
hfg : f =ᶠ[l] g
⊢ SuperpolynomialDecay l k g

Tactic:
fun z =>
  (hf z).congr' (EventuallyEq.mul (EventuallyEq.refl l _) hfg)

Premises used: Filter.EventuallyEq.mul, Filter.EventuallyEq.refl, HPow.hPow, Asymptotics.SuperpolynomialDecay, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
hfg : ∀ (x : α), f x = g x
⊢ SuperpolynomialDecay l k g

Tactic:
fun z =>
  (hf z).congr fun x => (congr_arg fun a => k x ^ z * a) <| hfg x

Premises used: HMul.hMul, congr_arg, HPow.hPow, Asymptotics.SuperpolynomialDecay, Filter.Tendsto.congr
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
inst_1 : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * 0 a) l (𝓝 0)

Tactic:
simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

Premises used: tendsto_const_nhds, Pi.zero_apply, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * (f + g) a) l (𝓝 0)

Tactic:
simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)

Premises used: Pi.add_apply, Filter.Tendsto.add, mul_add, add_zero
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * (f * g) a) l (𝓝 0)

Tactic:
simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)

Premises used: mul_assoc, pow_zero, MulZeroClass.mul_zero, Filter.Tendsto.mul, OfNat.ofNat, one_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * (fun (n : α) ↦ f n * c) a) l (𝓝 0)

Tactic:
simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)

Premises used: MulZeroClass.zero_mul, mul_assoc, Filter.Tendsto.mul_const
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
⊢ SuperpolynomialDecay l k fun (n : α) ↦ c * f n

Tactic:
(hf.mul_const c).congr fun _ => mul_comm _ _

Premises used: Asymptotics.SuperpolynomialDecay.congr, mul_comm, Asymptotics.SuperpolynomialDecay.mul_const
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen[inst] s
hs0 : 0 ∈ s
x : α
hx : Membership.mem (γ := Set α) ((fun (a : α) ↦ k a ^ (z + 1) * f a) ⁻¹' s) x
⊢ Membership.mem (γ := Set α) ((fun (a : α) ↦ k a ^ z * (k * f) a) ⁻¹' s) x

Tactic:
simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ] using hx

Premises used: Pi.mul_apply, pow_succ, mul_assoc, Set.mem_preimage
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (f * k)

Tactic:
hf.param_mul.congr fun _ => mul_comm _ _

Premises used: Asymptotics.SuperpolynomialDecay.congr, mul_comm, Asymptotics.SuperpolynomialDecay.param_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f)

Tactic:
simpa only [one_mul, pow_zero] using hf

Premises used: pow_zero, one_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f)

Tactic:
simpa only [pow_succ', mul_assoc] using hn.param_mul

Premises used: mul_assoc, Asymptotics.SuperpolynomialDecay.param_mul, pow_succ'
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f)
succ : ∀ (n : ℕ) (hn : SuperpolynomialDecay l k (k ^ n * f)), SuperpolynomialDecay l k (k ^ (n + 1) * f)
⊢ SuperpolynomialDecay l k (k ^ n * f)

Tactic:
induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul

Premises used: mul_assoc, pow_zero, pow_succ', one_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n)

Tactic:
(hf.param_pow_mul n).congr fun _ => mul_comm _ _

Premises used: Asymptotics.SuperpolynomialDecay.param_pow_mul, Asymptotics.SuperpolynomialDecay.congr, HPow.hPow, mul_comm
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousAdd β
inst_3 : ContinuousMul β
hf : SuperpolynomialDecay l k f
p_1 p q : β[X]
hp : SuperpolynomialDecay l k fun (x : α) ↦ eval (k x) p * f x
hq : SuperpolynomialDecay l k fun (x : α) ↦ eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun (x : α) ↦ eval (k x) (p + q) * f x

Tactic:
simpa [add_mul] using hp.add hq

Premises used: add_mul, Asymptotics.SuperpolynomialDecay.add
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousAdd β
inst_3 : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun (x : α) ↦ eval (k x) ((monomial n : (a : β) → β[X]) c) * f x

Tactic:
simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c

Premises used: mul_assoc, Asymptotics.SuperpolynomialDecay.param_pow_mul, Asymptotics.SuperpolynomialDecay.const_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : ContinuousAdd β
inst_3 : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
⊢ SuperpolynomialDecay l k fun (x : α) ↦ f x * eval (k x) p

Tactic:
(hf.polynomial_mul p).congr fun _ => mul_comm _ _

Premises used: Polynomial.eval, Asymptotics.SuperpolynomialDecay.congr, mul_comm, Asymptotics.SuperpolynomialDecay.polynomial_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
h : ∀ (hx' : 0 ≤ k x), k x ^ z * g x ≤ k x ^ z * f x
⊢ 0 x ≤ k x → k x ^ z * g x ≤ k x ^ z * f x

Tactic:
(hx' : 0 ≤ k x)
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
hx' : 0 ≤ k x
ha : 0 ≤ k x ^ z
⊢ k x ^ z * g x ≤ k x ^ z * f x

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ 0 x ≤ k x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ k b ^ z * g b ≤ k b ^ z * f b) x} x}
            x}
      a
h₁ : ∀ (a : α), g a ≤ f a → 0 a ≤ k a → k a ^ z * g a ≤ k a ^ z * f a
h₂ : ∀ (x : α) (hx : g x ≤ f x) (hx' : 0 ≤ k x), k x ^ z * g x ≤ k x ^ z * f x
⊢ ∀ᶠ (b : α) in l, k b ^ z * g b ≤ k b ^ z * f b

Tactic:
filter_upwards [hfg, hk] with x hx (hx' : 0 ≤ k x) using by gcongr
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
h : ∀ (hx' : 0 ≤ k x), k x ^ z * f x ≤ k x ^ z * g' x
⊢ 0 x ≤ k x → k x ^ z * f x ≤ k x ^ z * g' x

Tactic:
(hx' : 0 ≤ k x)
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst : TopologicalSpace β
inst_1 : CommSemiring β
inst_2 : PartialOrder β
inst_3 : IsOrderedRing β
inst_4 : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
hx' : 0 ≤ k x
ha : 0 ≤ k x ^ z
⊢ k x ^ z * f x ≤ k x ^ z * g' x

Tactic:
gcongr