awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
h : Tendsto f l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
zero_mul (0 : β) ▸ this.mul h

Premises used: MulZeroClass.zero_mul, Eq.rec, Filter.Tendsto.mul, 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_1 : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z) l (𝓝 0)
h : Tendsto f l (𝓝 0)
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
exact zero_mul (0 : β) ▸ this.mul h
-- 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
hf : SuperpolynomialDecay l k f
z : ℤ
rw :
  ∀ (hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) (z z_1 : ℤ),
    Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
⊢ SuperpolynomialDecay l k fun (a : α) ↦ k a ^ z * f a

Tactic:
rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢

Premises used: Asymptotics.superpolynomialDecay_iff_zpow_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
hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)

Tactic:
fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => ?_)

Premises used: Filter.Tendsto.eventually_ne_atTop, Filter.Eventually.mono, HAdd.hAdd, Filter.Tendsto.congr', 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
hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
refine : ∀ (z' : ℤ) (x : α) (hx : k x ≠ 0), k x ^ (z' + z) * f x = (fun (a : α) ↦ k a ^ z' * (k a ^ z * f a)) x
⊢ ∀ (z_1 : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)

Tactic:
refine fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => ?_)

Premises used: Filter.Tendsto.eventually_ne_atTop, Filter.Eventually.mono, HAdd.hAdd, Filter.Tendsto.congr', 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
hf : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z z' : ℤ
x : α
hx : k x ≠ 0
⊢ k x ^ (z' + z) * f x = (fun (a : α) ↦ k a ^ z' * (k a ^ z * f a)) x

Tactic:
simp [zpow_add₀ hx, mul_assoc]

Premises used: mul_assoc, zpow_add₀
-- 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
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun (a : α) ↦ f a * k a ^ z

Tactic:
(hf.param_zpow_mul hk z).congr fun _ => mul_comm _ _

Premises used: Asymptotics.SuperpolynomialDecay.congr, HPow.hPow, mul_comm, Asymptotics.SuperpolynomialDecay.param_zpow_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
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)

Tactic:
simpa using hf.param_zpow_mul hk (-1)

Premises used: Asymptotics.SuperpolynomialDecay.param_zpow_mul, OfNat.ofNat, Neg.neg
-- 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
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (f * k⁻¹)

Tactic:
(hf.inv_param_mul hk).congr fun _ => mul_comm _ _

Premises used: Asymptotics.SuperpolynomialDecay.congr, Inv.inv, Asymptotics.SuperpolynomialDecay.inv_param_mul, mul_comm
-- 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 (k * f)
x : α
hx : k x ≠ 0
⊢ (k⁻¹ * (k * f)) x = f x

Tactic:
simp [← mul_assoc, inv_mul_cancel₀ hx]

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 * k) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk

Premises used: mul_comm, Asymptotics.superpolynomialDecay_param_mul_iff
-- 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 (HPow.hPow (β := ℕ) k 0 * f) ↔ SuperpolynomialDecay l k f

Tactic:
simp
-- 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
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ (n + 1) * f) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [pow_succ, ← mul_comm k, mul_assoc,
      superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

Premises used: HMul.hMul, pow_succ, mul_assoc, HPow.hPow, mul_comm, Asymptotics.superpolynomialDecay_param_mul_iff
-- 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
n : ℕ
zero : SuperpolynomialDecay l k (HPow.hPow (β := ℕ) k 0 * f) ↔ SuperpolynomialDecay l k f
succ :
  ∀ (n : ℕ) (hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f),
    SuperpolynomialDecay l k (k ^ (n + 1) * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simpa [pow_succ, ← mul_comm k, mul_assoc,
      superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

Premises used: HMul.hMul, pow_succ, mul_assoc, HPow.hPow, mul_comm, Asymptotics.superpolynomialDecay_param_mul_iff
-- 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
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

Tactic:
simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n

Premises used: mul_comm, Asymptotics.superpolynomialDecay_param_pow_mul_iff
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
⊢ SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Tendsto (β := ℝ) (fun (a : α) ↦ ‖k a ^ n * f a‖) l (𝓝 0)

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

Premises used: Iff.mpr, tendsto_zero_iff_norm_tendsto_zero, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
⊢ (∀ (n : ℕ), Tendsto (β := ℝ) (fun (a : α) ↦ ‖k a ^ n * f a‖) l (𝓝 0)) ↔
    SuperpolynomialDecay (β := ℝ) l (fun (a : α) ↦ ‖k a‖) fun (a : α) ↦ ‖f a‖

Tactic:
simp [SuperpolynomialDecay]

Premises used: Asymptotics.SuperpolynomialDecay
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
(superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans ?_

Premises used: Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero, Iff.trans
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
refine :
  (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
refine (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans ?_

Premises used: Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero, Iff.trans
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ ∀ᶠ (x : α) in l, k x ≠ 0

Tactic:
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
⟨fun h z => ?_, fun h z => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
refine_1 :
  ∀ (h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) (z : ℤ),
    IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
refine_2 :
  ∀ (h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z) (z : ℤ),
    Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
⊢ (∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)) ↔
    ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
refine ⟨fun h z => ?_, fun h z => ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_

Premises used: Filter.Eventually.mono, absurd, Asymptotics.isBigO_of_div_tendsto_nhds, zpow_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
refine_1 : Tendsto (f / fun (a : α) ↦ k a ^ z) l (𝓝 0)
⊢ IsBigO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
refine isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz ↦ absurd hxz (zpow_ne_zero _ hx)) 0 ?_

Premises used: Filter.Eventually.mono, absurd, Asymptotics.isBigO_of_div_tendsto_nhds, zpow_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun (a : α) ↦ k a ^ z)⁻¹ x = k x ^ (-z)

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)

Tactic:
have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)
refine_1 : Tendsto ((fun (a : α) ↦ k a ^ (-z)) * f) l (𝓝 0)
⊢ Tendsto (f / fun (a : α) ↦ k a ^ z) l (𝓝 0)

Tactic:
rw [div_eq_mul_inv, mul_comm f, this]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)
⊢ Tendsto ((fun (a : α) ↦ k a ^ (-z)) * f) l (𝓝 0)

Tactic:
h (-z)

Premises used: Neg.neg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
this : Eq (α := (a : α) → β) (fun (a : α) ↦ k a ^ z)⁻¹ fun (a : α) ↦ k a ^ (-z)
⊢ Tendsto ((fun (a : α) ↦ k a ^ (-z)) * f) l (𝓝 0)

Tactic:
exact h (-z)

Premises used: Neg.neg
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
refine_2 : IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (a : α) ↦ k a ^ z * f a) fun (a : α) ↦ (k a)⁻¹
⊢ Tendsto.{u_1, u_2} (β := β) (fun (a : α) ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
suffices (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹ from
      IsBigO.trans_tendsto this hk.inv_tendsto_atTop
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (a : α) ↦ k a ^ z * f a) fun (a : α) ↦ (k a)⁻¹

Tactic:
((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
refine_2 : IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ k x ^ z * k x ^ (-(z + 1))) fun (a : α) ↦ (k a)⁻¹
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (a : α) ↦ k a ^ z * f a) fun (a : α) ↦ (k a)⁻¹

Tactic:
refine ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans ?_

Premises used: Asymptotics.IsBigO.mul, Asymptotics.IsBigO.trans, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Neg.neg, Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ k x ^ z * k x ^ (-(z + 1))) fun (a : α) ↦ (k a)⁻¹

Tactic:
.of_bound' <| hk0.mono fun a ha0 => ?_

Premises used: Filter.Eventually.mono, Asymptotics.IsBigO.of_bound'
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
refine_2 : ∀ (a : α) (ha0 : k a ≠ 0), ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ ‖(k a)⁻¹‖
⊢ IsBigO.{u_1, u_2, u_2} (E := β) (F := β) l (fun (x : α) ↦ k x ^ z * k x ^ (-(z + 1))) fun (a : α) ↦ (k a)⁻¹

Tactic:
refine .of_bound' <| hk0.mono fun a ha0 => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), IsBigO (F := β) l f fun (a : α) ↦ k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ ‖(k a)⁻¹‖

Tactic:
simp [← zpow_add₀ ha0]

Premises used: zpow_add₀
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
⟨fun h z => ?_, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩

Premises used: Iff.mpr, Asymptotics.IsLittleO.isBigO, Asymptotics.superpolynomialDecay_iff_isBigO, Iff.intro
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
refine : ∀ (h : SuperpolynomialDecay l k f) (z : ℤ), IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
refine ⟨fun h z => ?_, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ ∀ᶠ (x : α) in l, k x ≠ 0

Tactic:
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ Tendsto.{u_1, u_2} (β := β) (fun (x : α) ↦ 1 / k x) l (𝓝 0)

Tactic:
simpa using hk.inv_tendsto_atTop

Premises used: Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ IsLittleO (E := β) l (fun (x : α) ↦ 1) k

Tactic:
have : (fun _ : α => (1 : β)) =o[l] k :=
    isLittleO_of_tendsto' (hk0.mono fun x hkx hkx' => absurd hkx' hkx)
      (by simpa using hk.inv_tendsto_atTop)
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
⊢ IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)

Tactic:
simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)

Premises used: HSub.hSub, Asymptotics.superpolynomialDecay_iff_isBigO, Iff.mp, Asymptotics.IsLittleO.mul_isBigO, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
⊢ IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)

Tactic:
have : f =o[l] fun x : α => k x * k x ^ (z - 1) := by
    simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
-- Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Goal:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
inst_3 : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this_1 : IsLittleO (E := β) l (fun (x : α) ↦ 1) k
this : IsLittleO (F := β) l f fun (x : α) ↦ k x * k x ^ (z - 1)
⊢ IsLittleO (F := β) l f fun (a : α) ↦ k a ^ z

Tactic:
this.trans_isBigO <| IsBigO.of_bound' <| hk0.mono fun x hkx => le_of_eq ?_

Premises used: Filter.Eventually.mono, Asymptotics.IsBigO.of_bound', le_of_eq, Asymptotics.IsLittleO.trans_isBigO