-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProdFun_iUnion (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel η] (a : α)
    (f : ℕ → Set (β × γ)) (hf_meas : ∀ i, MeasurableSet (f i))
    (hf_disj : Pairwise (Disjoint on f)) :
    compProdFun κ η a (⋃ i, f i) = ∑' i, compProdFun κ η a (f i)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
⊢ (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})

Tactic:
ext1 b

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
b : β
⊢ (η (a, b)) {c | (b, c) ∈ ⋃ i, f i} = (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
⊢ (b, c) ∈ f i

Tactic:
exact hsi hcs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
hbci : {(b, c)} ⊆ f i
⊢ {(b, c)} ⊆ f j

Tactic:
rw [Set.singleton_subset_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
hbci : {(b, c)} ⊆ f i
⊢ (b, c) ∈ f j

Proof state:
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
⊢ c ∈ ⊥

Tactic:
have hbci : {(b, c)} ⊆ f i := by rw [Set.singleton_subset_iff]; exact hsi hcs

Result:
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
hbci : {(b, c)} ⊆ f i
⊢ c ∈ ⊥

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
i : ℕ
hm : MeasurableSet {p | (p.1.2, p.2) ∈ f i}
⊢ AEMeasurable (fun b => (η (a, b)) {c | (b, c) ∈ f i}) (κ a)

Tactic:
exact ((measurable_kernel_prod_mk_left hm).comp measurable_prod_mk_left).aemeasurable

Result:
no goals

Proof state:
case h.hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
i j : ℕ
hij : i ≠ j
s : Set γ
hsi : s ≤ (fun i => {c | (b, c) ∈ f i}) i
hsj : s ≤ (fun i => {c | (b, c) ∈ f i}) j
c : γ
hcs : c ∈ s
hbci : {(b, c)} ⊆ f i
hbcj : {(b, c)} ⊆ f j
⊢ c ∈ ⊥

Tactic:
simpa only [Set.bot_eq_empty, Set.le_eq_subset, Set.singleton_subset_iff,
  Set.mem_empty_iff_false] using hf_disj hij hbci hbcj

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
⊢ ∫⁻ (b : β), (η (a, b)) (⋃ i, {c | (b, c) ∈ f i}) ∂κ a = ∑' (i : ℕ), κ.compProdFun η a (f i)

Tactic:
rw [h_tsum, lintegral_tsum]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β), (η (a, a_1)) {c | (a_1, c) ∈ f i} ∂κ a = ∑' (i : ℕ), κ.compProdFun η a (f i)

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
⊢ ∀ (i : ℕ), AEMeasurable (fun b => (η (a, b)) {c | (b, c) ∈ f i}) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : ℕ → Set (β × γ)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf_disj : Pairwise (Disjoint on f)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β), (η (a, a_1)) {c | (a_1, c) ∈ f i} ∂κ a = ∑' (i : ℕ), κ.compProdFun η a (f i)

Tactic:
simp [compProdFun]

Result:
no goals