no goals
α : Type u_1
β : Type ?u.1613274
ι : Type ?u.1613277
E : Type u_2
F : Type ?u.1613283
𝕜 : Type ?u.1613286
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : BoundedSMul 𝕜 E
inst✝ : Fact (1 ≤ p)
f : { x // x ∈ simpleFunc E p μ }
⊢ ‖f‖ = ENNReal.toReal (snorm (↑(toSimpleFunc f)) p μ)
simpa [toLp_toSimpleFunc] using norm_toLp (toSimpleFunc f) (simpleFunc.memℒp f)