rotate_left
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ

case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ