α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ snorm (↑↑(Memℒp.toLp ↑↑f (_ : Memℒp (↑↑f) p))) p (Measure.restrict μ s) ≤ snorm (↑↑f) p μ
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ ‖Memℒp.toLp ↑↑f (_ : Memℒp (↑↑f) p)‖ ≤ ‖f‖
rw [Lp.norm_def, Lp.norm_def, ENNReal.toReal_le_toReal (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)]
case refine'_1
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ snorm (↑↑(Memℒp.toLp ↑↑f (_ : Memℒp (↑↑f) p))) p (Measure.restrict μ s) =
    snorm (↑↑f) p (Measure.restrict μ ?refine'_2)

case refine'_2
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ Set α
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ snorm (↑↑(Memℒp.toLp ↑↑f (_ : Memℒp (↑↑f) p))) p (Measure.restrict μ s) ≤ snorm (↑↑f) p μ
refine' (le_of_eq _).trans (snorm_mono_measure _ Measure.restrict_le_self)
no goals
case refine'_1
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ snorm (↑↑(Memℒp.toLp ↑↑f (_ : Memℒp (↑↑f) p))) p (Measure.restrict μ s) =
    snorm (↑↑f) p (Measure.restrict μ ?refine'_2)

case refine'_2
α : Type u_1
β : Type ?u.334371
E : Type u_2
F : Type ?u.334377
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
𝕜 : Type ?u.334386
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : ℝ≥0∞
μ : Measure α
s : Set α
f : { x // x ∈ Lp E p }
⊢ Set α
exact snorm_congr_ae (Memℒp.coeFn_toLp _)