-- 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:
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 ∈ ⊥

Tactic:
have hbcj : {(b, c)} ⊆ f j := by rw [Set.singleton_subset_iff]; exact hsj 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
hbcj : {(b, c)} ⊆ f j
⊢ c ∈ ⊥

Proof state:
case h.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)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
⊢ ∀ (i : ℕ), MeasurableSet {c | (b, c) ∈ f i}

Tactic:
exact fun i ↦ measurable_prod_mk_left (hf_meas i)

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
⊢ {(b, c)} ⊆ f i

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
⊢ (b, c) ∈ f i

Proof state:
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})

Tactic:
congr with c

Result:
case h.h.e_6.h.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 : β
c : γ
⊢ c ∈ {c | (b, c) ∈ ⋃ i, f i} ↔ c ∈ ⋃ 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})
h_tsum : (fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})) = fun b => ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}
i : ℕ
⊢ Measurable fun p => (p.1.2, p.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
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)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
⊢ (η (a, b)) (⋃ i, {c | (b, c) ∈ f i}) = ∑' (i : ℕ), (η (a, b)) {c | (b, c) ∈ f i}

Tactic:
rw [measure_iUnion]

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 : β
⊢ Pairwise (Disjoint on fun i => {c | (b, c) ∈ f i})

case h.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)
h_Union : (fun b => (η (a, b)) {c | (b, c) ∈ ⋃ i, f i}) = fun b => (η (a, b)) (⋃ i, {c | (b, c) ∈ f i})
b : β
⊢ ∀ (i : ℕ), MeasurableSet {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})
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)

Tactic:
intro i

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 : ℕ
⊢ AEMeasurable (fun b => (η (a, b)) {c | (b, c) ∈ f i}) (κ a)

Proof state:
case h.h.e_6.h.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 : β
c : γ
⊢ c ∈ {c | (b, c) ∈ ⋃ i, f i} ↔ c ∈ ⋃ i, {c | (b, c) ∈ f i}

Tactic:
simp only [Set.mem_iUnion, Set.iSup_eq_iUnion, Set.mem_setOf_eq]

Result:
no goals