no goals
α : Type u_1
β : Type ?u.1507935
ι : Type ?u.1507938
E : Type u_2
F : Type ?u.1507944
𝕜 : Type ?u.1507947
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
f g : α →ₛ E
hf : Memℒp (↑f) p
hg : Memℒp (↑g) p
⊢ toLp (f - g) (_ : Memℒp (↑f - fun a => ↑g a) p) = toLp f hf - toLp g hg
simp only [sub_eq_add_neg, ← toLp_neg, ← toLp_add]