cases hpq with
| inl hpq =>
  simp [hpq.left, hpq.right, -snorm_exponent_top] at *
  refine snorm_le_snorm_mul_snorm_top 1 hf g (fun u v => u * v) ?_
  refine Filter.eventually_of_forall ?_
  intro x
  simp
  exact nnnorm_mul_le (f x) (g x)
| inr hpq =>
  simp [hpq.left, hpq.right, -snorm_exponent_top] at *
  refine snorm_le_snorm_top_mul_snorm 1 f hg (fun u v => u * v) ?_
  refine Filter.eventually_of_forall ?_
  intro x
  simp
  exact nnnorm_mul_le (f x) (g x)
case 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 = 1 ∧ q = ⊤ ∨ p = ⊤ ∧ q = 1
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
no goals