no goals
α : Type u_3
E : Type u_2
F : Type ?u.3098262
G : Type ?u.3098265
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
β : Type u_1
mβ : MeasurableSpace β
f : α → β
g : β → E
hg : AEStronglyMeasurable g (Measure.map f μ)
hf : AEMeasurable f
⊢ Memℒp g p ↔ Memℒp (g ∘ f) p
simp [Memℒp, snorm_map_measure hg hf, hg.comp_aemeasurable hf, hg]