-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma setIntegral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ} (hA : MeasurableSet A) :
    ∫ x in A, density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal

Proof state:
case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
h : ((κ a) (A ×ˢ s)).toReal + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal - ((κ a) (A ×ˢ s)).toReal

Tactic:
rw [eq_tsub_iff_add_eq_of_le, add_comm]

Result:
case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
h : ((κ a) (A ×ˢ s)).toReal + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ((κ a) (A ×ˢ s)).toReal + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal

case compl
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A✝ : Set γ
this✝ : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = ((κ a) (A ×ˢ s)).toReal
h : ((κ a) (A ×ˢ s)).toReal + ∫ (x : γ) in Aᶜ, κ.density ν a x s ∂ν a = ((κ a) (univ ×ˢ s)).toReal
this : Aᶜ ×ˢ s = univ ×ˢ s \ A ×ˢ s
⊢ ((κ a) (A ×ˢ s)).toReal ≤ ((κ a) (univ ×ˢ s)).toReal

Proof state:
case iUnion
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = ((κ a) (f i ×ˢ s)).toReal
⊢ (∑' (a_1 : ℕ), (κ a) (f a_1 ×ˢ s)).toReal = ((κ a) ((⋃ i, f i) ×ˢ s)).toReal

Tactic:
congr

Result:
case iUnion.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s | ∃ n, MeasurableSet s}
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq : ∀ (i : ℕ), ∫ (x : γ) in f i, κ.density ν a x s ∂ν a = ((κ a) (f i ×ˢ s)).toReal
⊢ ∑' (a_1 : ℕ), (κ a) (f a_1 ×ˢ s) = (κ a) ((⋃ i, f i) ×ˢ s)