ι : Type ?u.197158
ι' : Type ?u.197161
α : Type u_2
β : Type u_1
γ : Type ?u.197170
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
this : Tendsto (fun x => -f x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
ι : Type ?u.197158
ι' : Type ?u.197161
α : Type u_2
β : Type u_1
γ : Type ?u.197170
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
have : Tendsto (fun x => -f x * g x) l atTop :=
  (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop hg