-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem _root_.Measurable.measure_of_isPiSystem {μ : α → Measure β} [∀ a, IsFiniteMeasure (μ a)]
    {S : Set (Set β)} (hgen : ‹MeasurableSpace β› = .generateFrom S) (hpi : IsPiSystem S)
    (h_basic : ∀ s ∈ S, Measurable fun a ↦ μ a s) (h_univ : Measurable fun a ↦ μ a univ) :
    Measurable μ

Proof state:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s : Set β
f : ℕ → Set β
hfd : Pairwise (Function.onFun Disjoint f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), Measurable fun b => (μ b) (f i)
⊢ Measurable fun b => (μ b) (⋃ i, f i)

Tactic:
simpa only [measure_iUnion hfd hfm] using .ennreal_tsum ihf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => (μ b) s

Tactic:
induction s, hs using MeasurableSpace.induction_on_inter hgen hpi with
| empty => simp
| basic s hs => exact h_basic s hs
| compl s hsm ihs =>
  simp only [measure_compl hsm (measure_ne_top _ _)]
  exact h_univ.sub ihs
| iUnion f hfd hfm ihf =>
  simpa only [measure_iUnion hfd hfm] using .ennreal_tsum ihf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
⊢ Measurable μ

Tactic:
rw [measurable_measure]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
⊢ ∀ (s : Set β), MeasurableSet s → Measurable fun b => (μ b) s

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
⊢ ∀ (s : Set β), MeasurableSet s → Measurable fun b => (μ b) s

Tactic:
intro s hs

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => (μ b) s

Proof state:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s✝ s : Set β
hsm : MeasurableSet s
ihs : Measurable fun b => (μ b) s
⊢ Measurable fun b => (μ b) sᶜ

Tactic:
simp only [measure_compl hsm (measure_ne_top _ _)]

Result:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s✝ s : Set β
hsm : MeasurableSet s
ihs : Measurable fun b => (μ b) s
⊢ Measurable fun b => (μ b) univ - (μ b) s

Proof state:
case empty
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s : Set β
⊢ Measurable fun b => (μ b) ∅

Tactic:
simp

Result:
no goals

Proof state:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s✝ s : Set β
hs : s ∈ S
⊢ Measurable fun b => (μ b) s

Tactic:
exact h_basic s hs

Result:
no goals

Proof state:
case compl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst✝ : ∀ (a : α), IsFiniteMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable fun a => (μ a) s
h_univ : Measurable fun a => (μ a) univ
s✝ s : Set β
hsm : MeasurableSet s
ihs : Measurable fun b => (μ b) s
⊢ Measurable fun b => (μ b) univ - (μ b) s

Tactic:
exact h_univ.sub ihs

Result:
no goals