case intro.intro
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
⊢ Tendsto (fun x => ‖v x‖) l atTop
rcases huv.exists_pos with ⟨c, hc, hcuv⟩
case intro.intro
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop
case intro.intro
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : IsBigOWith c l u v
⊢ Tendsto (fun x => ‖v x‖) l atTop
rw [IsBigOWith] at hcuv
case h.e'_3.h
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c
case intro.intro
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (fun x => ‖v x‖) l atTop
convert Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)
no goals
case h.e'_3.h
𝕜 : Type u_2
inst✝ : NormedLinearOrderedField 𝕜
α : Type u_1
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (fun x => ‖u x‖) l atTop
c : ℝ
hc : 0 < c
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x✝ : α
⊢ ‖v x✝‖ = c * ‖v x✝‖ / c
rw [mul_div_cancel_left _ hc.ne.symm]