ι : Type ?u.175674
ι' : Type ?u.175677
α : Type u_2
β : Type u_1
γ : Type ?u.175686
inst✝ : StrictOrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun x => f x * g x
ι : Type ?u.175674
ι' : Type ?u.175677
α : Type u_2
β : Type u_1
γ : Type ?u.175686
inst✝ : StrictOrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
refine' tendsto_atTop_mono' _ _ hg
no goals
ι : Type ?u.175674
ι' : Type ?u.175677
α : Type u_2
β : Type u_1
γ : Type ?u.175686
inst✝ : StrictOrderedSemiring α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atTop
⊢ g ≤ᶠ[l] fun x => f x * g x
filter_upwards [hg.eventually (eventually_ge_atTop 0),
  hf.eventually (eventually_ge_atTop 1)]with _ using le_mul_of_one_le_left