simp [hpq.left, hpq.right, -snorm_exponent_top] at *
case inr.inr
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq✝ : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : E → 𝕜
hf : AEStronglyMeasurable f μ
g : E → 𝕜
hg : AEStronglyMeasurable g μ
hpq : p = ⊤ ∧ q = 1
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
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 μ