simp
case inr.inl
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq✝ hpq : True
x : E
⊢ ‖(fun u v => u * v) (f x) (g x)‖₊ ≤ ‖f x‖₊ * ‖g x‖₊
case inr.inl
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq✝ hpq : True
x : E
⊢ ‖f x * g x‖₊ ≤ ‖f x‖₊ * ‖g x‖₊