ι : Type ?u.198322
ι' : Type ?u.198325
α : Type u_2
β : Type u_1
γ : Type ?u.198334
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x => -f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
ι : Type ?u.198322
ι' : Type ?u.198325
α : Type u_2
β : Type u_1
γ : Type ?u.198334
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atTop
have : Tendsto (fun x => -f x * -g x) l atTop :=
  (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop (tendsto_neg_atBot_atTop.comp hg)
no goals
ι : Type ?u.198322
ι' : Type ?u.198325
α : Type u_2
β : Type u_1
γ : Type ?u.198334
inst✝ : StrictOrderedRing α
l : Filter β
f g : β → α
hf : Tendsto f l atBot
hg : Tendsto g l atBot
this : Tendsto (fun x => -f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
simpa only [neg_mul_neg] using this