awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 μ
have refine : ∀ (s : Set β) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ ((map f b : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: refine measurable_of_measurable_coe _ fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 α) ↦ ((map f b : Measure β) : (a : Set β) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : Measure α) ↦ (b : (a : Set α) → ℝ≥0∞) (f ⁻¹' s)
Tactic: simp_rw [map_apply hf hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Measurable.{u_1, u_1} (α := α) (β := Measure α) dirac
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((dirac b : Measure α) : (a : Set α) → ℝ≥0∞) s
Tactic: refine measurable_of_measurable_coe _ fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ((dirac b : Measure α) : (a : Set α) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (b : α) ↦ s.indicator 1 b
Tactic: simp_rw [dirac_apply' _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ ∫⁻ (x : α), f x ∂μ
have 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∞)
Tactic: simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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∞)
have 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∞)
Tactic: refine .iSup fun n => Finset.measurable_fun_sum _ fun i _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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∞)
have refine : Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦
  (μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.eapprox f n) : (a : α) → ℝ≥0∞) {i})
Tactic: refine Measurable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ 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) ⋯)
have simp_rw : ∫⁻ (μ : Measure α), ∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m =
  ∑' (i : ℕ), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m
Tactic: simp_rw [measure_iUnion h hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ ∫⁻ (μ : Measure α), ∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m =
    ∑' (i : ℕ), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) (f i) ∂m
have hf₁ : ∀ (i : ℕ), AEMeasurable (β := ℝ≥0∞) (fun (a : Measure α) ↦ (a : (a : Set α) → ℝ≥0∞) (f i)) m
Tactic: apply lintegral_tsum
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
⊢ ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤ (m.join : (a : Set α) → ℝ≥0∞) s
have rw : ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m ≤
  ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m.join : (a : Set α) → ℝ≥0∞) t
Tactic: rw [measure_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 α)
⊢ (c • m).join = c • m.join
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((c • m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((c • m.join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
⊢ (sum m).join = sum fun (i : ι) ↦ (m i).join
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
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∞)
have h : Eq (α := ℝ≥0∞) (((sum m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), ((m i).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply _ hs, join_apply hs, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((sum m).join : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (i : ι) ↦ (m i).join : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂sum m = ∑' (i : ι), ∫⁻ (μ : Measure α), (μ : (a : Set α) → ℝ≥0∞) s ∂m i
Tactic: simp_rw [sum_apply _ hs, join_apply hs, lintegral_sum_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ join (dirac μ) = μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((join (dirac μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
s : Set α
hs : s ∈ ae m.join
⊢ s ∈ (ae m).bind ae
have 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
Tactic: rcases exists_measurable_superset_of_null hs with ⟨t, hst, htm, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (hypothesis)
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∞)
⊢ s ∈ (ae m).bind ae
have ht₁ : (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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ s ∈ (ae m).bind ae
have rw : {a : Measure α | s ∈ ae a} ∈ ae m
Tactic: rw [mem_bind']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (join 0) 0
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((join 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have 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
Tactic: wlog hfm : Measurable f generalizing f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have wlog : ∀ {f : α → ℝ≥0∞} (hf : AEMeasurable f m.join) (hfm : Measurable f),
  ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Tactic: wlog hfm : Measurable f generalizing f
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have inr : ∀ (g : α → ℝ≥0∞) (hgm : Measurable g) (hfg : f =ᶠ[ae m.join] g),
  ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Tactic: rcases hf with ⟨g, hgm, hfg⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have inr : ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Tactic: rw [lintegral_congr_ae hfg, this hgm.aemeasurable hgm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have 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
Tactic: simp_rw [lintegral_eq_iSup_eapprox_lintegral hfm, SimpleFunc.lintegral,
    join_apply (SimpleFunc.measurableSet_preimage _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
have 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)
Tactic: refine
      this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ ⨆ (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
have 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 μ
Tactic: refine
      this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n))
        (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' {r})) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hfm : Measurable f
⊢ ⨆ (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
have ℕ : ∀ (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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
have 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)
Tactic: rw [lintegral_iSup _ hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ ⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r ∈ s n, r * f n r μ ∂m
have rw₁ : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (μ : Measure α) ↦ ∑ r ∈ s n, r * f n r μ
Tactic: rw [lintegral_iSup _ hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 μ
⊢ Eq (α := ℝ≥0∞) (⨆ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m)
    (⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 μ
⊢ 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
have e_s : ∀ (n : ℕ), ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
Tactic: funext n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
have e_s : Eq (α := ℝ≥0∞) (∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) (∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m)
Tactic: rw [lintegral_finsetSum (s n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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)
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
have e_s₁ : ∀ b ∈ s n, Measurable (β := ℝ≥0∞) fun (a : Measure α) ↦ b * f n b a
Tactic: rw [lintegral_finsetSum (s n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0∞
m : Measure (Measure α)
⊢ ∫⁻ (x : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have 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
Tactic: rcases exists_measurable_le_lintegral_eq (join m) f with ⟨g, hgm, hgf, hfg_int⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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 : α), f x ∂m.join ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have rw : ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
Tactic: rw [hfg_int, lintegral_join hgm.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ ∫⁻ (μ : Measure α), ∫⁻ (x : α), g x ∂μ ∂m ≤ ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
have hfg : ∀ (x : Measure α) (x : α), g x ≤ f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : AEMeasurable f m
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
have rw : (join (map f m) : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.GiryMonad (goal)
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
⊢ (m.bind f : (a : Set β) → ℝ≥0∞) s = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
have rw₁ : ∫⁻ (μ : Measure β), (μ : (a : Set β) → ℝ≥0∞) s ∂map f m = ∫⁻ (a : α), (f a : (a : Set β) → ℝ≥0∞) s ∂m
Tactic: rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf]