no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.992421
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
K K' : ℝ≥0
f : α → β
g : β → γ
hg : LipschitzWith K g
hg' : AntilipschitzWith K' g
g0 : g 0 = 0
⊢ Integrable (g ∘ f) ↔ Integrable f
simp [← memℒp_one_iff_integrable, hg.memℒp_comp_iff_of_antilipschitz hg' g0]