-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
@[simp]
lemma bind_dirac_eq_map (m : Measure α) {f : α → β} (hf : Measurable f) :
    m.bind (fun x ↦ Measure.dirac (f x)) = m.map f

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (dirac (f a)) s ∂m = (map f m) s

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => dirac (f x)

Tactic:
swap

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => dirac (f x)

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (dirac (f a)) s ∂m = (map f m) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => dirac (f x)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (dirac (f a)) s ∂m = (map f m) s

Tactic:
simp_rw [dirac_apply' _ hs]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator 1 (f a) ∂m = (map f m) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), s.indicator 1 (f a) ∂m = (map f m) s

Tactic:
rw [← lintegral_map _ hf, lintegral_indicator_one hs]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (s.indicator 1)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (s.indicator 1)

Tactic:
exact measurable_const.indicator hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
⊢ (m.bind fun x => dirac (f x)) = map f m

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (m.bind fun x => dirac (f x)) s = (map f m) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (m.bind fun x => dirac (f x)) s = (map f m) s

Tactic:
rw [bind_apply hs]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), (dirac (f a)) s ∂m = (map f m) s

case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun x => dirac (f x)