α : Type u_1
β : Type ?u.1731961
γ : Type ?u.1731964
δ : Type ?u.1731967
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
α : Type u_1
β : Type ?u.1731961
γ : Type ?u.1731964
δ : Type ?u.1731967
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
f : α → ℝ≥0∞
⊢ (∫⁻ (x : α) in insert a s, f x ∂μ) = f a * ↑↑μ {a} + ∫⁻ (x : α) in s, f x ∂μ
rw [← union_singleton, lintegral_union (measurableSet_singleton a), lintegral_singleton,
  add_comm]
no goals
α : Type u_1
β : Type ?u.1731961
γ : Type ?u.1731964
δ : Type ?u.1731967
m : MeasurableSpace α
μ ν : Measure α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : ¬a ∈ s
f : α → ℝ≥0∞
⊢ Disjoint s {a}
rwa [disjoint_singleton_right]