cases ENNReal.conjugate_cases hpq with
| inl hpq =>
  rcases hpq with ⟨hp, hq⟩
  have hp' : p ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact ENNReal.one_le_of_conjugate hpq
  have hq' : q ≠ 0
  . refine ne_of_gt (lt_of_lt_of_le zero_lt_one ?_)
    exact ENNReal.one_le_of_conjugate' hpq
  rw [snorm_eq_lintegral_rpow_nnnorm hp' hp.right]
  rw [snorm_eq_lintegral_rpow_nnnorm hq' hq.right]
  rw [snorm_one_eq_lintegral_nnnorm]
  simp [-one_div]
  refine le_trans ?_ (NNReal.lintegral_mul_le_Lp_mul_Lq ?_ ?_ ?_)
  rotate_left
  . exact ENNReal.isConjugateExponent_toReal hpq hp.right hq.right
  . exact hf.nnnorm.aemeasurable
  . exact hg.nnnorm.aemeasurable
  simp
  refine lintegral_mono ?_
  intro x
  simp
  norm_cast
  exact nnnorm_mul_le (f x) (g x)
| inr hpq =>
  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)
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 μ
⊢ snorm (f * g) 1 μ ≤ snorm f p μ * snorm g q μ
no goals