case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      ↑↑(Measure.prod μ ν) s < ⊤ →
        (∫ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
          ∫ (x : α), ∫ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ

case h_add
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f →
        Integrable g →
          ((∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
            ((∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) →
              (∫ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ

case h_closed
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ IsClosed {f | (∫ (z : α × β), ↑↑f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ}

case h_ae
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᶠ[ae (Measure.prod μ ν)] g →
      Integrable f →
        ((∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
          (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ (f : α × β → E), Integrable f → (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
apply Integrable.induction
case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ ν) s < ⊤
⊢ (∫ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫ (x : α), ∫ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ
case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ (c : E) ⦃s : Set (α × β)⦄,
    MeasurableSet s →
      ↑↑(Measure.prod μ ν) s < ⊤ →
        (∫ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
          ∫ (x : α), ∫ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ
intro c s hs h2s
case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ ν) s < ⊤
⊢ ENNReal.toReal (↑↑(Measure.prod μ ν) s) • c = ENNReal.toReal (∫⁻ (a : α), ↑↑ν (Prod.mk a ⁻¹' s) ∂μ) • c
case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ ν) s < ⊤
⊢ (∫ (z : α × β), indicator s (fun x => c) z ∂Measure.prod μ ν) =
    ∫ (x : α), ∫ (y : β), indicator s (fun x => c) (x, y) ∂ν ∂μ
simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp,
  integral_indicator (measurable_prod_mk_left hs), set_integral_const, integral_smul_const,
  integral_toReal (measurable_measure_prod_mk_left hs).aemeasurable
    (ae_measure_lt_top hs h2s.ne)]
no goals
case h_ind
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
c : E
s : Set (α × β)
hs : MeasurableSet s
h2s : ↑↑(Measure.prod μ ν) s < ⊤
⊢ ENNReal.toReal (↑↑(Measure.prod μ ν) s) • c = ENNReal.toReal (∫⁻ (a : α), ↑↑ν (Prod.mk a ⁻¹' s) ∂μ) • c
rw [prod_apply hs]
case h_add
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
i_f : Integrable f
i_g : Integrable g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
hg : (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
case h_add
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : α × β → E⦄,
    Disjoint (support f) (support g) →
      Integrable f →
        Integrable g →
          ((∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
            ((∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) →
              (∫ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
rintro f g - i_f i_g hf hg
no goals
case h_add
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
i_f : Integrable f
i_g : Integrable g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
hg : (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), (f + g) z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), (f + g) (x, y) ∂ν ∂μ
simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
no goals
case h_closed
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ IsClosed {f | (∫ (z : α × β), ↑↑f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ}
exact isClosed_eq continuous_integral continuous_integral_integral
case h_ae
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
case h_ae
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
⊢ ∀ ⦃f g : α × β → E⦄,
    f =ᶠ[ae (Measure.prod μ ν)] g →
      Integrable f →
        ((∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ) →
          (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
rintro f g hfg - hf
case h.e'_2
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (z : α × β), f z ∂Measure.prod μ ν

case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
case h_ae
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ
convert hf using 1
no goals
case h.e'_2
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (z : α × β), g z ∂Measure.prod μ ν) = ∫ (z : α × β), f z ∂Measure.prod μ ν
exact integral_congr_ae hfg.symm
case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (fun x => ∫ (y : β), g (x, y) ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), f (x, y) ∂ν
case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫ (x : α), ∫ (y : β), g (x, y) ∂ν ∂μ) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
refine' integral_congr_ae _
case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∀ᵐ (x : α) ∂μ,
    (∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) → (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ (fun x => ∫ (y : β), g (x, y) ∂ν) =ᶠ[ae μ] fun x => ∫ (y : β), f (x, y) ∂ν
refine' (ae_ae_of_ae_prod hfg).mp _
case h.e'_3.hp
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∀ (x : α),
    (∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) → (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
case h.e'_3
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∀ᵐ (x : α) ∂μ,
    (∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) → (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
apply eventually_of_forall
case h.e'_3.hp
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
x : α
hfgx : ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)
⊢ (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
case h.e'_3.hp
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
⊢ ∀ (x : α),
    (∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)) → (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
intro x hfgx
no goals
case h.e'_3.hp
α : Type u_1
α' : Type ?u.2445862
β : Type u_2
β' : Type ?u.2445868
γ : Type ?u.2445871
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type ?u.2446136
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
hfg : f =ᶠ[ae (Measure.prod μ ν)] g
hf : (∫ (z : α × β), f z ∂Measure.prod μ ν) = ∫ (x : α), ∫ (y : β), f (x, y) ∂ν ∂μ
x : α
hfgx : ∀ᵐ (y : β) ∂ν, f (x, y) = g (x, y)
⊢ (fun x => ∫ (y : β), g (x, y) ∂ν) x = (fun x => ∫ (y : β), f (x, y) ∂ν) x
exact integral_congr_ae (ae_eq_symm hfgx)