rw [snorm_eq_lintegral_rpow_nnnorm hq' hq.right]
case inl.intro
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 μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ snorm (f * g) 1 μ ≤ (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) * snorm g q μ
case inl.intro
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 μ
hp : 1 < p ∧ p ≠ ⊤
hq : 1 < q ∧ q ≠ ⊤
hp' : p ≠ 0
hq' : q ≠ 0
⊢ snorm (f * g) 1 μ ≤
    (∫⁻ (x : E), ↑‖f x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) *
      (∫⁻ (x : E), ↑‖g x‖₊ ^ ENNReal.toReal q ∂μ) ^ (1 / ENNReal.toReal q)