-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem lintegral_join {m : Measure (Measure α)} {f : α → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ x, f x ∂join m = ∫⁻ μ, ∫⁻ x, f x ∂μ ∂m

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m

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

Result:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ 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 fun n μ =>
    ∑ r ∈ (fun n => (SimpleFunc.eapprox f n).range) n, r * (fun n r μ => μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r μ

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ 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:
intro s f hf hm

Result:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ 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

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r ∈ s n, r * f n r μ

Tactic:
fun_prop

Result:
no goals

Proof state:
case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable fun a => b * f n b a

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

Result:
no goals

Proof state:
case e_s
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ (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

Result:
case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ 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

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ 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 ((fun n r μ => μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r)

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

Result:
no goals

Proof state:
case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ 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 _ _)]

Result:
no goals

Proof state:
case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ 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

Tactic:
rw [lintegral_finset_sum (s n)]

Result:
case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m

case e_s.h
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
n : ℕ
⊢ ∀ b ∈ s n, Measurable fun a => b * f n b a

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ n, ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

Tactic:
congr

Result:
case e_s
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ (fun n => ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) = fun n => ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

Proof state:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ 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]

Result:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ ⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ n, ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m

α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r ∈ s n, r * f n r μ