-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integrable_measure_prod_mk_left {s : Set (α × β)} (hs : MeasurableSet s)
    (h2s : (μ.prod ν) s ≠ ∞) : Integrable (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
x : α
hx : ν (Prod.mk x ⁻¹' s) ≠ ⊤
⊢ ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)

Tactic:
simp [ofReal_toReal, hx]

Result:
no goals

Proof state:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ (fun a => ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal) =ᶠ[ae μ] fun a => ν (Prod.mk a ⁻¹' s)

Tactic:
filter_upwards [ae_measure_lt_top hs h2s] with x hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
x : α
hx : ν (Prod.mk x ⁻¹' s) < ⊤
⊢ ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ HasFiniteIntegral (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ

Tactic:
simp_rw [hasFiniteIntegral_iff_enorm, enorm_eq_ofReal toReal_nonneg]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ < ⊤

Tactic:
convert h2s.lt_top using 1

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = (μ.prod ν) s

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = (μ.prod ν) s

Tactic:
rw [prod_apply hs]

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ ∫⁻ (a : α), ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal ∂μ = ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

Tactic:
apply lintegral_congr_ae

Result:
case h.e'_3.h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ (fun a => ENNReal.ofReal (ν (Prod.mk a ⁻¹' s)).toReal) =ᶠ[ae μ] fun a => ν (Prod.mk a ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ Integrable (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ

Tactic:
refine ⟨(measurable_measure_prod_mk_left hs).ennreal_toReal.aemeasurable.aestronglyMeasurable, ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
⊢ HasFiniteIntegral (fun x => (ν (Prod.mk x ⁻¹' s)).toReal) μ

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
x : α
hx : ν (Prod.mk x ⁻¹' s) < ⊤
⊢ ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)

Tactic:
rw [lt_top_iff_ne_top] at hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ.prod ν) s ≠ ⊤
x : α
hx : ν (Prod.mk x ⁻¹' s) ≠ ⊤
⊢ ENNReal.ofReal (ν (Prod.mk x ⁻¹' s)).toReal = ν (Prod.mk x ⁻¹' s)