obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ (fun x => f (i, x)) =O[l] g
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => f (i, x)) =O[l] g