case hst
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ Disjoint (s \ t) t

case ht
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ MeasurableSet t

case hfs
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ IntegrableOn (fun x => f x) (s \ t)

case hft
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ IntegrableOn (fun x => f x) t
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ (∫ (x : α) in s \ t, f x ∂μ) = (∫ (x : α) in s, f x ∂μ) - ∫ (x : α) in t, f x ∂μ
rw [eq_sub_iff_add_eq, ← integral_union, diff_union_of_subset hts]
no goals
case hst
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ Disjoint (s \ t) t

case ht
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ MeasurableSet t

case hfs
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ IntegrableOn (fun x => f x) (s \ t)

case hft
α : Type u_1
β : Type ?u.7261
E : Type u_2
F : Type ?u.7267
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
ht : MeasurableSet t
hfs : IntegrableOn f s
hts : t ⊆ s
⊢ IntegrableOn (fun x => f x) t
exacts [disjoint_sdiff_self_left, ht, hfs.mono_set (diff_subset _ _), hfs.mono_set hts]