awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α) ↦ f x ≤ g' 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 * f b ≤ k b ^ z * g' b) x} x}
            x}
      a
h₁ : ∀ (a : α), f a ≤ g' a → 0 a ≤ k a → k a ^ z * f a ≤ k a ^ z * g' a
h₂ : ∀ (x : α) (hx : f x ≤ g' x) (hx' : 0 ≤ k x), k x ^ z * f x ≤ k x ^ z * g' x
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' 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 : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
⊢ SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)

Tactic:
⟨fun h z => (tendsto_zero_iff_abs_tendsto_zero _).1 (h z), fun h z =>
    (tendsto_zero_iff_abs_tendsto_zero _).2 (h z)⟩

Premises used: Iff.mpr, HMul.hMul, tendsto_zero_iff_abs_tendsto_zero, HPow.hPow, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
simp_rw :
  (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
    ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a| ^ n * |f a|) l (𝓝 0)
simp_rw₁ :
  (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n| * |f a|) l (𝓝 0)) ↔
    ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a| ^ n * |f a|) l (𝓝 0)
⊢ (∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) ↔
    SuperpolynomialDecay.{u_1, u_2} (β := β) l (fun (a : α) ↦ |k a|) fun (a : α) ↦ |f a|

Tactic:
simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]

Premises used: abs_mul, Asymptotics.SuperpolynomialDecay, abs_pow
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
rw :
  ∀ (hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)) (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f)
    (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * g a|) l (𝓝 0)
⊢ SuperpolynomialDecay l k g

Tactic:
rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢

Premises used: Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * g a|) l (𝓝 0)

Tactic:
fun z =>
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
      (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)

Premises used: HMul.hMul, tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, Filter.Eventually.mono, HPow.hPow, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
refine : ∀ (z : ℕ) (x : α) (hx : (abs ∘ g) x ≤ (abs ∘ f) x), |k x ^ z * g x| ≤ |k x ^ z * f x|
⊢ ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * g a|) l (𝓝 0)

Tactic:
refine fun z =>
    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
      (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, Filter.Eventually.mono, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z * g x| = |k x ^ z| * |g x|

Tactic:
abs_mul (k x ^ z) (g x)

Premises used: abs_mul, HPow.hPow
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
hbc : |g x| ≤ |f x|
⊢ |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 : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|

Tactic:
hx

Premises used: abs
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|

Tactic:
exact hx
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |f x| = |k x ^ z * f x|

Tactic:
(abs_mul (k x ^ z) (f x)).symm

Premises used: abs_mul, HPow.hPow, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : ∀ (n : ℕ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
x₁ : |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|

Tactic:
calc
    |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
    _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
    _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm

Premises used: abs_mul, HPow.hPow, Eq.symm
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst : TopologicalSpace β
inst_1 : CommRing β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : ∀ (x : α), |g x| ≤ |f x|
⊢ SuperpolynomialDecay l k g

Tactic:
hf.trans_eventually_abs_le (Eventually.of_forall hfg)

Premises used: Filter.Eventually.of_forall, Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun (n : α) ↦ f n * c
x : α
⊢ f x * c * c⁻¹ = f x

Tactic:
simp [mul_assoc, mul_inv_cancel₀ hc0]

Premises used: mul_inv_cancel₀, mul_assoc
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun (n : α) ↦ c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x

Tactic:
simp [← mul_assoc, inv_mul_cancel₀ hc0]

Premises used: mul_assoc, inv_mul_cancel₀
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|

Tactic:
⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
      (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => ?_⟩

Premises used: Iff.mpr, Filter.Tendsto.isBoundedUnder_le, Filter.Tendsto.abs, Iff.intro, Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h :
  ∀ (h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|) (z : ℕ),
    Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|

Tactic:
refine
    ⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
      (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
obtain :
  ∀ (m : β) (hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m),
    Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
obtain ⟨m, hm⟩ := h (z + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)

Tactic:
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)

Tactic:
have h2 : Tendsto (fun a : α => |(k a)⁻¹| * m) l (𝓝 0) :=
    zero_mul m ▸
      Tendsto.mul_const m ((tendsto_zero_iff_abs_tendsto_zero _).1 hk.inv_tendsto_atTop)
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
      ((eventually_map.1 hm).mp ?_)

Premises used: HMul.hMul, tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, Filter.eventually_map, Filter.Eventually.mp, HPow.hPow, Iff.mp, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
tendsto_of_tendsto_of_tendsto_of_le_of_le' :
  ∀ᶠ (x : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |k a ^ z * f a|) l (𝓝 0)

Tactic:
refine
    tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (Eventually.of_forall fun x => abs_nonneg _)
      ((eventually_map.1 hm).mp ?_)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le', Filter.Eventually.of_forall, Filter.eventually_map, Filter.Eventually.mp, Iff.mp, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
(hk.eventually_ne_atTop 0).mono fun x hk0 hx => ?_

Premises used: Filter.Tendsto.eventually_ne_atTop, Filter.Eventually.mono, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
refine :
  ∀ (x : α) (hk0 : k x ≠ 0) (hx : (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m), |k x ^ z * f x| ≤ |(k x)⁻¹| * m
⊢ ∀ᶠ (x : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
refine (hk.eventually_ne_atTop 0).mono fun x hk0 hx => ?_

Premises used: Filter.Tendsto.eventually_ne_atTop, Filter.Eventually.mono, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)

Premises used: Eq.trans_le, Inv.inv, mul_le_mul_of_nonneg_left, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
refine : |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m

Tactic:
refine Eq.trans_le ?_ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)

Premises used: Eq.trans_le, Inv.inv, mul_le_mul_of_nonneg_left, abs_nonneg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l fun (a : α) ↦ |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ |k a ^ (z + 1) * f a|) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x m
h1 : Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 0) l (𝓝 0)
h2 : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun (x1 x2 : β) ↦ x1 ≤ x2) |k x ^ (z + 1) * f x| m
rw : |k x ^ z * f x| = |(k x)⁻¹ * (k x ^ (z + 1) * f x)|
rw₁ : |k x ^ z * f x| = |(k x)⁻¹ * k x ^ (z + 1) * f x|
rw₂ : |k x ^ z * f x| = |(k x)⁻¹ * (k x * k x ^ z) * f x|
rw₃ : |k x ^ z * f x| = |(k x)⁻¹ * k x * k x ^ z * f x|
rw₄ : |k x ^ z * f x| = |1 * k x ^ z * f x|
rw₅ rw₆ : |k x ^ z * f x| = |k x ^ z * f x|
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|

Tactic:
rw [← abs_mul, ← mul_assoc, pow_succ', ← mul_assoc, inv_mul_cancel₀ hk0, one_mul]

Premises used: mul_assoc, abs_mul, inv_mul_cancel₀, pow_succ', one_mul
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ n * f a) l (𝓝 0)

Tactic:
simpa only [zpow_natCast] using h (n : ℤ)

Premises used: zpow_natCast, Nat.cast
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
refine : ∀ (h : SuperpolynomialDecay l k f) (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
refine ⟨fun h z => ?_, fun h n => by simpa only [zpow_natCast] using h (n : ℤ)⟩
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
pos : ∀ (hz : 0 ≤ z), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
neg : ∀ (hz : z < 0), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
by_cases! hz : 0 ≤ z
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ 0 ≤ z

Tactic:
hz
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
pos :
  ∀ (z : ℕ), LE.le.{u_2} (α := Filter β) (Filter.map (fun (a : α) ↦ HPow.hPow (β := ℤ) (k a) (↑z : ℤ) * f a) l) (𝓝 0)
⊢ LE.le.{u_2} (α := Filter β) (Filter.map (fun (a : α) ↦ k a ^ z * f a) l) (𝓝 0)

Tactic:
lift z to ℕ using hz
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℕ
⊢ LE.le.{u_2} (α := Filter β) (Filter.map (fun (a : α) ↦ HPow.hPow (β := ℤ) (k a) (↑z : ℤ) * f a) l) (𝓝 0)

Tactic:
simpa using h z
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)

Tactic:
have : Tendsto (fun a => k a ^ z) l (𝓝 0) :=
      Tendsto.comp (tendsto_zpow_atTop_zero hz) hk
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Tactic:
simpa using h 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : TopologicalSpace β
inst_1 : Field β
inst_2 : LinearOrder β
inst_3 : IsStrictOrderedRing β
inst_4 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Tactic:
have h : Tendsto f l (𝓝 0) := by simpa using h 0