awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : 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 (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
h_univ : Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ
s : Set β
hs : MeasurableSet s
empty : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) ∅
basic : ∀ (s : Set β) (hs : s ∈ S), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s
compl :
  ∀ (s : Set β) (hsm : MeasurableSet s) (ihs : Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) sᶜ
iUnion :
  ∀ (f : ℕ → Set β) (hfd : Pairwise (Function.onFun Disjoint f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
    (ihf : ∀ (i : ℕ), Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (f i)),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) (⋃ (i : ℕ), f i)
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ (μ b : (a : Set β) → ℝ≥0∞) 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 .tsum ihf

Premises used: Compl.compl, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : α → Measure β
inst : ∀ (a : α), IsProbabilityMeasure (μ a)
S : Set (Set β)
hgen : mβ = MeasurableSpace.generateFrom S
hpi : IsPiSystem S
h_basic : ∀ s ∈ S, Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) s
⊢ Measurable (β := ℝ≥0∞) fun (a : α) ↦ (μ a : (a : Set β) → ℝ≥0∞) univ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (μ : Measure α) ↦ map f μ

Tactic:
measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
refine :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ ((map f b : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (μ : Measure α) ↦ map f μ

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
simp_rw : Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ (b : (a : Set α) → ℝ≥0∞) (f ⁻¹' s)
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ ((map f b : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
simp_rw [map_apply hf hs]

Premises used: MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ (b : (a : Set α) → ℝ≥0∞) (f ⁻¹' s)

Tactic:
measurable_coe (hf hs)

Premises used: MeasureTheory.Measure.measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ (b : (a : Set α) → ℝ≥0∞) (f ⁻¹' s)

Tactic:
exact measurable_coe (hf hs)

Premises used: MeasureTheory.Measure.measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Measurable.{u_1, u_1} (α := α) (β := Measure α) dirac

Tactic:
measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((dirac b : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ Measurable.{u_1, u_1} (α := α) (β := Measure α) dirac

Tactic:
refine measurable_of_measurable_coe _ fun s hs => ?_

Premises used: MeasureTheory.Measure.measurable_of_measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 b
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((dirac b : Measure α) : (a : Set α) → ℝ≥0∞) s

Tactic:
simp_rw [dirac_apply' _ hs]

Premises used: MeasureTheory.Measure.dirac_apply'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 b

Tactic:
measurable_one.indicator hs

Premises used: Measurable.indicator, measurable_one
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 b

Tactic:
exact measurable_one.indicator hs

Premises used: Measurable.indicator, measurable_one
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
simp :
  Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ ∫⁻ (x : α), f x ∂μ

Tactic:
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)

Tactic:
.iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_

Premises used: Measurable.iSup, MeasureTheory.SimpleFunc.eapprox, Finset.measurable_fun_sum, MeasureTheory.SimpleFunc.range
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
refine :
  ∀ (n : ℕ),
    ∀ i ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
      Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
        HMul.hMul (β := ℝ≥0∞) i
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i}) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        HMul.hMul (β := ℝ≥0∞) x
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) : ℝ≥0∞)

Tactic:
refine .iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
h : i ∈ SimpleFunc.range (SimpleFunc.eapprox f n)
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    HMul.hMul (β := ℝ≥0∞) i
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i}) : ℝ≥0∞)

Tactic:
Measurable.const_mul ?_ _

Premises used: Measurable.const_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
h : i ∈ SimpleFunc.range (SimpleFunc.eapprox f n)
refine :
  Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i})
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    HMul.hMul (β := ℝ≥0∞) i
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i}) : ℝ≥0∞)

Tactic:
refine Measurable.const_mul ?_ _

Premises used: Measurable.const_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
h : i ∈ SimpleFunc.range (SimpleFunc.eapprox f n)
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i})

Tactic:
measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
h : i ∈ SimpleFunc.range (SimpleFunc.eapprox f n)
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
    (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i})

Tactic:
exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
⊢ Eq (α := ℝ≥0∞) ((fun (s : Set α) (x : MeasurableSet s) ↦ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m) ∅ ⋯) 0

Tactic:
simp only [measure_empty, lintegral_const, zero_mul]

Premises used: MeasureTheory.lintegral_const, MulZeroClass.zero_mul, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
simp_rw :
  ∫⁻ (μ : Measure α), ∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m =
    ∑' (i : ℕ), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m
⊢ Eq (α := ℝ≥0∞)
    ((fun (s : Set α) (x : MeasurableSet s) ↦ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m) (⋃ (i : ℕ), f i) ⋯)
    (∑' (i : ℕ), (fun (s : Set α) (x : MeasurableSet s) ↦ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m) (f i) ⋯)

Tactic:
simp_rw [measure_iUnion h hf]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
hf₁ : ∀ (i : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : Measure α) ↦ (a : (a : Set α) → ℝ≥0∞) (f i)) m
⊢ ∫⁻ (μ : Measure α), ∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m =
    ∑' (i : ℕ), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m

Tactic:
apply lintegral_tsum

Premises used: MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : Measure α) ↦ (a : (a : Set α) → ℝ≥0∞) (f i)) m

Tactic:
(measurable_coe (hf i)).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Function.onFun Disjoint f)
i : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : Measure α) ↦ (a : (a : Set α) → ℝ≥0∞) (f i)) m

Tactic:
exact (measurable_coe (hf i)).aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (m.join : (a : Set α) → ℝ≥0∞) s = ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m

Tactic:
Measure.ofMeasurable_apply s hs

Premises used: MeasureTheory.Measure.ofMeasurable_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
rw :
  ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤
    ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m.join : (a : Set α) → ℝ≥0∞) t
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤ (m.join : (a : Set α) → ℝ≥0∞) s

Tactic:
rw [measure_eq_iInf]

Premises used: MeasureTheory.measure_eq_iInf
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) t ∂m

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤
    ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m.join : (a : Set α) → ℝ≥0∞) t

Tactic:
exact le_iInf₂ fun t hst ↦ le_iInf fun htm ↦ join_apply htm ▸ by gcongr

Premises used: le_iInf, le_iInf₂
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((c • m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((c • m.join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (c • m).join = c • m.join

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((c • m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((c • m.join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((sum m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sum fun (i : ι) ↦ (m i).join : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (sum m).join = sum fun (i : ι) ↦ (m i).join

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((sum m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), ((m i).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂sum m =
    ∑' (i : ι), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m i
⊢ Eq (α := ℝ≥0∞) (((sum m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (m i).join : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [sum_apply _ hs, join_apply hs, lintegral_sum_measure]

Premises used: MeasureTheory.Measure.sum_apply, MeasureTheory.Measure.join_apply, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((join (dirac μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ join (dirac μ) = μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((join (dirac μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hs, lintegral_dirac', measurable_coe]

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.lintegral_dirac'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
rcases :
  ∀ (t : Set α) (hst : sᶜ ⊆ t) (htm : MeasurableSet t)
    (ht : Eq (α := ℝ≥0∞) ((m.join : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)), s ∈ (ae m).bind ae
⊢ s ∈ (ae m).bind ae

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, hst, htm, ht⟩

Premises used: MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : Eq (α := ℝ≥0∞) ((m.join : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae m).EventuallyEq (β := ℝ≥0∞) (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) t) 0

Tactic:
rw [join_apply htm, lintegral_eq_zero_iff (measurable_coe htm)] at ht

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.Measure.measurable_coe, MeasureTheory.Measure.join_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (ae m).EventuallyEq (β := ℝ≥0∞) (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) t) 0
rw : {a : Measure α | s ∈ ae a} ∈ ae m
⊢ s ∈ (ae m).bind ae

Tactic:
rw [mem_bind']

Premises used: Filter.mem_bind'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (ae m).EventuallyEq (β := ℝ≥0∞) (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) t) 0
⊢ {a : Measure α | s ∈ ae a} ∈ ae m

Tactic:
ht.mono fun _ ↦ measure_mono_null hst

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.measure_mono_null, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
t : Set α
hst : sᶜ ⊆ t
htm : MeasurableSet t
ht : (ae m).EventuallyEq (β := ℝ≥0∞) (fun (μ : Measure α) ↦ (μ : (a : Set α) → ℝ≥0∞) t) 0
⊢ {a : Measure α | s ∈ ae a} ∈ ae m

Tactic:
exact ht.mono fun _ ↦ measure_mono_null hst

Premises used: MeasureTheory.measure_mono_null, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
p : α → Prop
h : ∀ᵐ (a : α) ∂m.join, p a
⊢ ∀ᵐ (μ : Measure α) ∂m, ∀ᵐ (a : α) ∂μ, p a

Tactic:
le_ae_join m h

Premises used: MeasureTheory.Measure.le_ae_join, Set.Mem, Filter.Eventually, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure (Measure α)
f : α → β
h : AEMeasurable f m.join
⊢ ∀ᵐ (μ : Measure α) ∂m, AEMeasurable f μ

Tactic:
let ⟨g, hgm, hg⟩ := h; (ae_ae_of_ae_join hg).mono fun _μ hμ ↦ ⟨g, hgm, hμ⟩

Premises used: MeasureTheory.ae, AEMeasurable, Filter.Eventually, _private.0.AEMeasurable.ae_of_join.match_1, Filter.Eventually.mono, And.intro, Exists.intro, MeasureTheory.Measure.ae_ae_of_ae_join
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
h : AEMeasurable f m.join
⊢ AEMeasurable (β := ℝ≥0∞) (fun (μ : Measure α) ↦ ∫⁻ (a : α), f a ∂μ) m

Tactic:
let ⟨g, hgm, hfg⟩ := h
  ⟨fun μ ↦ ∫⁻ a, g a ∂μ, measurable_lintegral hgm,
    (ae_ae_of_ae_join hfg).mono fun _ ↦ lintegral_congr_ae⟩

Premises used: AEMeasurable, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, _private.0.MeasureTheory.Measure.aemeasurable_lintegral.match_1, And.intro, Exists.intro, MeasureTheory.Measure.ae_ae_of_ae_join, MeasureTheory.Measure.measurable_lintegral, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((join 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure α) (join 0) 0

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((join 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : Measure (Measure α)) ↦ (b.join : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [join_apply hs, measurable_lintegral (measurable_coe hs)]

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.Measure.measurable_lintegral, MeasureTheory.Measure.join_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
inr :
  ∀
    (this :
      ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
        ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m)
    (hfm : ¬Measurable f), ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
wlog :
  ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
    ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
wlog hfm : Measurable f generalizing f

Premises used: Measurable
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
this :
  ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
    ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
inr :
  ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hfg : f =ᶠ[ae m.join] g),
    ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rcases hf with ⟨g, hgm, hfg⟩
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
    ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᶠ[ae m.join] g
inr : ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
this :
  ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
    ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
hfm : ¬Measurable f
g : α → ℝ≥0∞
hgm : Measurable g
hfg : f =ᶠ[ae m.join] g
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
lintegral_congr_ae <| (ae_ae_of_ae_join hfg).mono fun μ hμ ↦
      .symm <| lintegral_congr_ae hμ

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Measure.ae_ae_of_ae_join, Eq.symm