obtain ⟨t, htl, ht⟩ := hC.exists_mem
case 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 : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
⊢ g =O[l] fun x => f (i, x)
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 : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
⊢ g =O[l] fun x => f (i, x)