obtain ⟨C, hC⟩ := hf.bound
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ