no goals
α : Type u_1
β : Type ?u.6755
inst✝ : Preorder α
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p => Ixx p.fst p.snd) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (smallSets (l₂ ⊓ l₂'))
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1