awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
simp_rw :
  ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        x *
          ∫⁻ (μ : Measure α),
            (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) ∂m =
    ∫⁻ (μ : 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∞) ∂m
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
simp_rw [lintegral_eq_iSup_eapprox_lintegral hfm, SimpleFunc.lintegral,
    join_apply (SimpleFunc.measurableSet_preimage _ _)]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.measurableSet_preimage, MeasureTheory.Measure.join_apply, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        x *
          ∫⁻ (μ : Measure α),
            (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) ∂m =
    ∫⁻ (μ : 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∞) ∂m

Tactic:
this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_

Premises used: MeasureTheory.SimpleFunc.eapprox, Set.preimage, MeasureTheory.SimpleFunc.range, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
refine_1 :
  ∀ (n : ℕ) (r : ℝ≥0∞),
    Measurable.{u_1, 0} (α := Measure α) (β := ℝ≥0∞)
      ((fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
        n r)
refine_2 :
  Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦
    ∑ r ∈ (fun (n : ℕ) ↦ SimpleFunc.range (SimpleFunc.eapprox f n)) n,
      r *
        (fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
            ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
          n r μ
⊢ ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        x *
          ∫⁻ (μ : Measure α),
            (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) ∂m =
    ∫⁻ (μ : 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∞) ∂m

Tactic:
refine
      this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_

Premises used: MeasureTheory.SimpleFunc.eapprox, Set.preimage, MeasureTheory.SimpleFunc.range, Singleton.singleton, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ ∀ (n : ℕ) (r : ℝ≥0∞),
    Measurable.{u_1, 0} (α := Measure α) (β := ℝ≥0∞)
      ((fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
        n r)

Tactic:
fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.measurableSet_preimage, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ ∀ (n : ℕ) (r : ℝ≥0∞),
    Measurable.{u_1, 0} (α := Measure α) (β := ℝ≥0∞)
      ((fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
        n r)

Tactic:
exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)

Premises used: MeasureTheory.Measure.measurable_coe, MeasureTheory.SimpleFunc.measurableSet_preimage
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦
    ∑ r ∈ (fun (n : ℕ) ↦ SimpleFunc.range (SimpleFunc.eapprox f n)) n,
      r *
        (fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
            ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
          n r μ

Tactic:
fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl

Premises used: MeasureTheory.SimpleFunc.lintegral, le_rfl, Monotone, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦
    ∑ r ∈ (fun (n : ℕ) ↦ SimpleFunc.range (SimpleFunc.eapprox f n)) n,
      r *
        (fun (n : ℕ) (r : ℝ≥0∞) (μ : Measure α) ↦
            ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞))
          n r μ

Tactic:
exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl

Premises used: le_rfl, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.SimpleFunc.lintegral_mono
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
ℕ :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
⊢ ⨆ (n : ℕ),
      ∑ x ∈ SimpleFunc.range (SimpleFunc.eapprox f n),
        x *
          ∫⁻ (μ : Measure α),
            (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {x}) ∂m =
    ∫⁻ (μ : 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∞) ∂m

Tactic:
suffices
    ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞), (∀ n r, Measurable (f n r)) →
      Monotone (fun n μ => ∑ r ∈ s n, r * f n r μ) →
      ⨆ n, ∑ r ∈ s n, r * ∫⁻ μ, f n r μ ∂m = ∫⁻ μ, ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m by
    refine
      this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_
    · exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
    · exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m)
    (⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m)
rw₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m

Tactic:
rw [lintegral_iSup _ hm]

Premises used: MeasureTheory.lintegral_iSup
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
e_s :
  Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) fun (n : ℕ) ↦
    ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m)
    (⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
e_s : ∀ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) fun (n : ℕ) ↦
    ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

Tactic:
funext n
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
e_s : Eq (α := ℝ≥0∞) (∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) (∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m)
e_s₁ : ∀ b ∈ s n, Measurable (β := ℝ≥0∞) fun (a : Measure α) ↦ b * f n b a
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

Tactic:
rw [lintegral_finsetSum (s n)]

Premises used: MeasureTheory.lintegral_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) (∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m)

Tactic:
simp_rw [lintegral_const_mul _ (hf _ _)]

Premises used: MeasureTheory.lintegral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable (β := ℝ≥0∞) fun (a : Measure α) ↦ b * f n b a

Tactic:
fun r _ => (hf _ _).const_mul _

Premises used: Measurable.const_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f_1 : α → ℝ≥0∞
hfm : Measurable f_1
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone.{0, u_1} (β := (μ : Measure α) → ℝ≥0∞) fun (n : ℕ) (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable (β := ℝ≥0∞) fun (a : Measure α) ↦ b * f n b a

Tactic:
exact fun r _ => (hf _ _).const_mul _

Premises used: Measurable.const_mul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
rcases :
  ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hgf : g ≤ f) (hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join),
    ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rcases exists_measurable_le_lintegral_eq (join m) f with ⟨g, hgm, hgf, hfg_int⟩

Premises used: MeasureTheory.Measure.join, MeasureTheory.exists_measurable_le_lintegral_eq
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
rw : ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
rw [hfg_int, lintegral_join hgm.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.lintegral_join
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
hfg : ∀ (x : Measure α) (x : α), g x ≤ f x
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
g : α → ℝ≥0∞
hgm : Measurable g
hgf : g ≤ f
hfg_int : ∫⁻ (a : α), f a ∂m.join = ∫⁻ (a : α), g a ∂m.join
x : Measure α
x_1 : α
⊢ g x_1 ≤ f x_1

Tactic:
apply hgf
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → Measure β
⊢ bind (mα := mα) 0 f = 0

Tactic:
simp [bind]

Premises used: MeasureTheory.Measure.bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
rw : (join (map f m) : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
rw₁ : ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
rw₂ rw₃ : ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m

Tactic:
rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.measurable_coe, MeasureTheory.Measure.bind, MeasureTheory.Measure.join_apply, MeasureTheory.lintegral_map'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
rw : ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m ≤ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s ≤ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m

Tactic:
rw [bind, join_apply hs]

Premises used: MeasureTheory.Measure.bind, MeasureTheory.Measure.join_apply
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m ≤ ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m

Tactic:
apply lintegral_map_le

Premises used: MeasureTheory.lintegral_map_le
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
p : β → Prop
hf : AEMeasurable f m
h : ∀ᵐ (b : β) ∂m.bind f, p b
⊢ ∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b

Tactic:
ae_of_ae_map hf <| ae_ae_of_ae_join h

Premises used: MeasureTheory.ae_of_ae_map, MeasureTheory.Measure.ae_ae_of_ae_join
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
x : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → γ
hf : AEMeasurable f m
hg : AEMeasurable g (m.bind f)
⊢ ∀ᵐ (a : α) ∂m, AEMeasurable g (f a)

Tactic:
ae_of_ae_map hf hg.ae_of_join

Premises used: AEMeasurable.ae_of_join, MeasureTheory.ae_of_ae_map
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → Measure β
h : f =ᶠ[ae μ] g
⊢ μ.bind f = μ.bind g

Tactic:
congrArg join <| map_congr h

Premises used: MeasureTheory.Measure.join, congrArg, MeasureTheory.Measure.bind, MeasureTheory.Measure.map_congr
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
ν : Measure β
⊢ (m.bind fun (x : α) ↦ ν) = HSMul.hSMul (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν

Tactic:
simp [bind]

Premises used: MeasureTheory.Measure.bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β) (m.bind fun (x : α) ↦ 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
⊢ Eq.{u_2 + 1} (α := Measure β) (m.bind 0) 0

Tactic:
bind_zero_right' m

Premises used: MeasureTheory.Measure.bind_zero_right'
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : α → Measure β
hg : Measurable g
⊢ Measurable.{u_1, u_2} (β := Measure β) fun (m : Measure α) ↦ m.bind g

Tactic:
measurable_join.comp (measurable_map _ hg)

Premises used: MeasureTheory.Measure.join, Measurable.comp, MeasureTheory.Measure.measurable_map, MeasureTheory.Measure.bind, MeasureTheory.Measure.ofMeasurable, MeasureTheory.Measure.measurable_join
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
g : α → Measure β
m : Measure (Measure α)
hg : AEMeasurable g m.join
⊢ AEMeasurable.{u_1, u_2} (β := Measure β) (fun (x : Measure α) ↦ x.bind g) m

Tactic:
let ⟨f, hfm, hf⟩ := hg
  ⟨(bind · f), measurable_bind' hfm, (ae_ae_of_ae_join hf).mono fun _ ↦ bind_congr_right⟩

Premises used: MeasureTheory.Measure.bind_congr_right, AEMeasurable, MeasureTheory.Measure.bind, _private.0.MeasureTheory.Measure.aemeasurable_bind.match_1, MeasureTheory.Measure.measurable_bind', Filter.Eventually.mono, And.intro, Exists.intro, MeasureTheory.Measure.ae_ae_of_ae_join
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable (_m := mα) f (sum fun (i : ι) ↦ m i)
simp_rw : join (map f (sum fun (i : ι) ↦ m i)) = sum fun (i : ι) ↦ join (map f (m i))
simp_rw₁ : Eq.{u_2 + 1} (α := Measure β) (join (sum fun (i : ι) ↦ map f (m i))) (sum fun (i : ι) ↦ join (map f (m i)))
⊢ bind (mα := mα) (sum fun (i : ι) ↦ m i) f = sum fun (i : ι) ↦ (m i).bind f

Tactic:
simp_rw [bind, map_sum h, join_sum]

Premises used: MeasureTheory.Measure.join_sum, MeasureTheory.Measure.map_sum, MeasureTheory.Measure.bind
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_3
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure α
f : α → Measure β
simp_rw : join (map f (c • m)) = c • join (map f m)
simp_rw₁ : (HSMul.hSMul (β := Measure (Measure β)) c (map f m)).join = c • join (map f m)
⊢ (c • m).bind f = c • m.bind f

Tactic:
simp_rw [bind, Measure.map_smul, join_smul]

Premises used: MeasureTheory.Measure.join_smul, MeasureTheory.Measure.bind, MeasureTheory.Measure.map_smul
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
μ : α → Measure β
f : β → ℝ≥0∞
hμ : AEMeasurable μ m
hf : AEMeasurable f (m.bind μ)
⊢ ∫⁻ (x : β), f x ∂m.bind μ = ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m

Tactic:
(lintegral_join hf).trans (lintegral_map' (aemeasurable_lintegral hf) hμ)

Premises used: MeasureTheory.Measure.aemeasurable_lintegral, MeasureTheory.Measure.bind, MeasureTheory.Measure.lintegral_join, MeasureTheory.lintegral_map', Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.GiryMonad
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
m : Measure α
μ : α → Measure β
⊢ ∫⁻ (x : β), f x ∂m.bind μ ≤ ∫⁻ (a : α), ∫⁻ (x : β), f x ∂μ a ∂m

Tactic:
(lintegral_join_le _ _).trans (lintegral_map_le _ _)

Premises used: MeasureTheory.Measure.bind, MeasureTheory.Measure.lintegral_join_le, MeasureTheory.lintegral_map_le, LE.le.trans