ι : Type ?u.196199
ι' : Type ?u.196202
α : Type u_2
β : Type u_1
γ : Type ?u.196211
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
this : Tendsto (fun x => f x * (Neg.neg ∘ g) x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
ι : Type ?u.196199
ι' : Type ?u.196202
α : Type u_2
β : Type u_1
γ : Type ?u.196211
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atTop
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atBot
have := hf.atTop_mul_atTop <| tendsto_neg_atBot_atTop.comp hg