-- 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✝
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 μ

Tactic:
swap

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 : ℕ), Measurable fun μ => ∑ r ∈ s n, r * f n r μ

α : 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

Proof state:
α : 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, ∑ 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

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

Result:
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)

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 μ