-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_eq_measure_prod (a : α) {s : Set β} (hs : MeasurableSet s)
    {t : Set Ω} (ht : MeasurableSet t) :
    ∫⁻ b in s, Kernel.condKernel κ (a, b) t ∂(Kernel.fst κ a) = κ a (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∀ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b

Tactic:
intro b

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
b : β
⊢ (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)

Tactic:
congr

Result:
case e_a.e_a
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ κ = κ.fst ⊗ₖ κ.condKernel

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a

Tactic:
have : ∀ b, Kernel.condKernel κ (a, b) {c | (b, c) ∈ s ×ˢ t}
    = s.indicator (fun b ↦ Kernel.condKernel κ (a, b) t) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
this : ∀ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a

Proof state:
case e_a.e_a
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ κ = κ.fst ⊗ₖ κ.condKernel

Tactic:
exact (κ.disintegrate _).symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
this : ∀ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a

Tactic:
simp_rw [this]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
this : ∀ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a =
    ∫⁻ (b : β), s.indicator (fun b => (κ.condKernel (a, b)) t) b ∂κ.fst a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)

Tactic:
rw [this, Kernel.compProd_apply (hs.prod ht)]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
b : β
⊢ (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b

Tactic:
by_cases hb : b ∈ s <;> simp [hb]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
this : ∀ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} = s.indicator (fun b => (κ.condKernel (a, b)) t) b
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a =
    ∫⁻ (b : β), s.indicator (fun b => (κ.condKernel (a, b)) t) b ∂κ.fst a

Tactic:
rw [lintegral_indicator hs]

Result:
no goals