obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
case intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g