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

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst

Tactic:
have : ∀ b, ρ.condKernel b (Prod.mk b ⁻¹' s ×ˢ t)
    = s.indicator (fun b ↦ ρ.condKernel b t) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
this : ∀ (b : β), (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
this : ∀ (b : β), (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst

Tactic:
simp_rw [this]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
this : ∀ (b : β), (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), s.indicator (fun b => (ρ.condKernel b) t) a ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

Tactic:
have : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t) := by
  congr; exact (ρ.disintegrate _).symm

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)

Tactic:
congr

Result:
case e_a
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ρ = ρ.fst ⊗ₘ ρ.condKernel

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∀ (b : β), (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b

Tactic:
intro b

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
b : β
⊢ (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst

Tactic:
classical
have : ∀ b, ρ.condKernel b (Prod.mk b ⁻¹' s ×ˢ t)
    = s.indicator (fun b ↦ ρ.condKernel b t) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]
simp_rw [this]
rw [lintegral_indicator hs]

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
b : β
⊢ (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b

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

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this✝ : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
this : ∀ (b : β), (ρ.condKernel b) (Prod.mk b ⁻¹' s ×ˢ t) = s.indicator (fun b => (ρ.condKernel b) t) b
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), s.indicator (fun b => (ρ.condKernel b) t) a ∂ρ.fst

Tactic:
rw [lintegral_indicator hs]

Result:
no goals

Proof state:
case e_a
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
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
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

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

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : ρ (s ×ˢ t) = (ρ.fst ⊗ₘ ρ.condKernel) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s ×ˢ t) ∂ρ.fst