-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_iff_isBigO (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k f ↔ ∀ z : ℤ, f =O[l] fun a : α => k a ^ z

Proof state:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] 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 ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun x => k x ^ z * k x ^ (-(z + 1))) =O[l] fun a => (k a)⁻¹

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

Result:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ ‖(k a)⁻¹‖

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z

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

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z

Proof state:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ Tendsto (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

Result:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z

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

Result:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] fun a => k a ^ z

case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)

Tactic:
rw [div_eq_mul_inv, mul_comm f, this]

Result:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto ((fun a => k a ^ (-z)) * f) l (𝓝 0)

Proof state:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹

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

Result:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun x => k x ^ z * k x ^ (-(z + 1))) =O[l] fun a => (k a)⁻¹

Proof state:
case refine_2
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] 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]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun a => k a ^ z)⁻¹ x = k x ^ (-z)

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto ((fun a => k a ^ (-z)) * f) l (𝓝 0)

Tactic:
exact h (-z)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z

Tactic:
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0

Result:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z

Proof state:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)

Tactic:
have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp

Result:
case refine_1
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)