no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.675870
G : Type ?u.675873
𝕜 : Type ?u.675876
p : ℝ≥0∞
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
inst✝² : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → ↑↑μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : { x // x ∈ simpleFunc E 1 μ }
⊢ setToL1S T (f - g) = setToL1S T f - setToL1S T g
rw [sub_eq_add_neg, setToL1S_add T h_zero h_add, setToL1S_neg h_zero h_add, sub_eq_add_neg]