α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (f : α × β → ℝ≥0∞), Measurable f → (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ ∀ (f : α × β → ℝ≥0∞), Measurable f → (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have m := @measurable_prod_mk_left
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ)
        (indicator s fun x => c)

case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) f →
            (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) g →
              (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f + g)

case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)) →
          (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) fun x =>
            ⨆ (n : ℕ), f n x
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (f : α × β → ℝ≥0∞), Measurable f → (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
refine' Measurable.ennreal_induction
  (P := fun f => (∫⁻ z, f z ∂μ.prod ν) = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ) _ _ _
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ)
        (indicator s fun x => c)
intro c s hs
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), indicator (Prod.mk x ⁻¹' s) (fun x => c) y ∂ν ∂μ
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ
conv_rhs =>
  enter [2, x, 2, y]
  rw [← indicator_comp_right, const_def, const_comp, ← const_def]
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) = ∫⁻ (x : α), c * ↑↑ν (Prod.mk x ⁻¹' s) ∂μ
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.5353233} {β : Type ?u.5353232} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), indicator (Prod.mk x ⁻¹' s) (fun x => c) y ∂ν ∂μ
conv_rhs =>
  enter [2, x]
  rw [lintegral_indicator _ (m (x := x) hs), lintegral_const,
    Measure.restrict_apply MeasurableSet.univ, univ_inter]
no goals
case refine'_1
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ (∫⁻ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) = ∫⁻ (x : α), c * ↑↑ν (Prod.mk x ⁻¹' s) ∂μ
simp [hs, lintegral_const_mul, measurable_measure_prod_mk_left (ν := ν) hs, prod_apply]
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), (f + g) (x, y) ∂ν ∂μ
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) f →
            (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) g →
              (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f + g)
rintro f g - hf _ h2f h2g
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), f z + g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), (f + g) (x, y) ∂ν ∂μ
simp only [Pi.add_apply]
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ((∫⁻ (a : α × β), f a ∂Measure.prod μ ν) + ∫⁻ (a : α × β), g a ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), f z + g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ
conv_lhs => rw [lintegral_add_left hf]
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ((∫⁻ (a : α × β), f a ∂Measure.prod μ ν) + ∫⁻ (a : α × β), g a ∂Measure.prod μ ν) =
    ∫⁻ (x : α), (∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν) + ∫⁻ (a : β), g (x, a) ∂ν ∂μ
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ((∫⁻ (a : α × β), f a ∂Measure.prod μ ν) + ∫⁻ (a : α × β), g a ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν ∂μ
conv_rhs => enter [2, x]; erw [lintegral_add_left (hf.comp (m (x := x)))]
no goals
case refine'_2
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
a✝ : Measurable g
h2f : (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
h2g : (∫⁻ (z : α × β), g z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), g (x, y) ∂ν ∂μ
⊢ ((∫⁻ (a : α × β), f a ∂Measure.prod μ ν) + ∫⁻ (a : α × β), g a ∂Measure.prod μ ν) =
    ∫⁻ (x : α), (∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν) + ∫⁻ (a : β), g (x, a) ∂ν ∂μ
simp [lintegral_add_left, Measurable.lintegral_prod_right', hf, h2f, h2g]
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)) →
          (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) fun x =>
            ⨆ (n : ℕ), f n x
intro f hf h2f h3f
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
have kf : ∀ x n, Measurable fun y => f n (x, y) := fun x n => (hf n).comp m
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
have k2f : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
have lf : ∀ n, Measurable fun x => ∫⁻ y, f n (x, y) ∂ν := fun n => (hf n).lintegral_prod_right'
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
l2f : Monotone fun n x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
have l2f : Monotone fun n x => ∫⁻ y, f n (x, y) ∂ν := fun i j hij x =>
  lintegral_mono (k2f x hij)
no goals
case refine'_3
α : Type u_1
α' : Type ?u.5352968
β : Type u_2
β' : Type ?u.5352974
γ : Type ?u.5352977
E : Type ?u.5352980
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => (∫⁻ (z : α × β), f z ∂Measure.prod μ ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)
kf : ∀ (x : α) (n : ℕ), Measurable fun y => f n (x, y)
k2f : ∀ (x : α), Monotone fun n y => f n (x, y)
lf : ∀ (n : ℕ), Measurable fun x => ∫⁻ (y : β), f n (x, y) ∂ν
l2f : Monotone fun n x => ∫⁻ (y : β), f n (x, y) ∂ν
⊢ (∫⁻ (z : α × β), (fun x => ⨆ (n : ℕ), f n x) z ∂Measure.prod μ ν) =
    ∫⁻ (x : α), ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν ∂μ
simp only [lintegral_iSup hf h2f, lintegral_iSup (kf _), k2f, lintegral_iSup lf l2f, h3f]