refine snorm_le_snorm_top_mul_snorm 1 f hg (fun u v => u * v) ?_
case inr.inr
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
⊢ snorm (f * g) 1 μ ≤ snorm f ⊤ μ * snorm g 1 μ
case inr.inr
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‖₊