no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1464610
G : Type ?u.1464613
𝕜 : Type ?u.1464616
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✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f
hg : Integrable g
⊢ setToFun μ T hT (f - g) = setToFun μ T hT f - setToFun μ T hT g
rw [sub_eq_add_neg, sub_eq_add_neg, setToFun_add hT hf hg.neg, setToFun_neg hT g]