awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
refine : map (Prod.map f g) (μ.prod τ) ≪ ν.prod υ
⊢ QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := β) fun (a : α) ↦ f a
⊢ Measurable f

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
funProp : inst_2 ≤ inst_2
funProp₁ : MeasurableEmbedding.{u_3, u_4} (β := ω) fun (a : γ) ↦ g a
⊢ Measurable g

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
rw : Measure.prod (map f μ) (map g τ) ≪ ν.prod υ
⊢ map (Prod.map f g) (μ.prod τ) ≪ ν.prod υ

Tactic:
rw [← map_prod_map _ _ (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_prod_map
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measure.prod (map f μ) (map g τ) ≪ ν.prod υ

Tactic:
hf.absolutelyContinuous.prod hg.absolutelyContinuous

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.prod, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst_3 : SFinite μ
inst_4 : SFinite τ
inst_5 : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ Measure.prod (map f μ) (map g τ) ≪ ν.prod υ

Tactic:
exact hf.absolutelyContinuous.prod hg.absolutelyContinuous

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.prod, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → γ
hf : AEMeasurable f (ν.prod μ)
⊢ AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))

Tactic:
rw [← Measure.prod_swap] at hf

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → γ
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))
⊢ AEMeasurable (β := γ) (fun (z : α × β) ↦ f z.swap) (μ.prod ν)

Tactic:
hf.comp_measurable measurable_swap

Premises used: AEMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst_3 : SFinite μ
inst_4 : SFinite ν
f : β × α → γ
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))
⊢ AEMeasurable (β := γ) (fun (z : α × β) ↦ f z.swap) (μ.prod ν)

Tactic:
exact hf.comp_measurable measurable_swap

Premises used: AEMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
hf : NullMeasurable f μ
⊢ NullMeasurable (β := γ) (fun (z : α × β) ↦ f z.1) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst

Premises used: MeasureTheory.NullMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : α → γ
hf : AEMeasurable f μ
⊢ AEMeasurable (β := γ) (fun (z : α × β) ↦ f z.1) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst

Premises used: AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : β → γ
hf : NullMeasurable f ν
⊢ NullMeasurable (β := γ) (fun (z : α × β) ↦ f z.2) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd

Premises used: MeasureTheory.NullMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
f : β → γ
hf : AEMeasurable f ν
⊢ AEMeasurable (β := γ) (fun (z : α × β) ↦ f z.2) (μ.prod ν)

Tactic:
hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd

Premises used: AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.Measure.quasiMeasurePreserving_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
obtain :
  ∀ (g : α × β → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae (μ.prod ν)] g),
    AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ

Tactic:
obtain ⟨g, hg, hfg⟩ := hf
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae (μ.prod ν)] g
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (y : β), g (x, y) ∂ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae (μ.prod ν)] g
refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) fun (x : α) ↦ ∫⁻ (y : β), g (x, y) ∂ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ

Tactic:
refine ⟨fun x ↦ ∫⁻ y, g (x, y) ∂ν, by fun_prop, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae (μ.prod ν)] g
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) fun (x : α) ↦ ∫⁻ (y : β), g (x, y) ∂ν

Tactic:
(ae_ae_of_ae_prod hfg).mono fun x hfg' ↦ lintegral_congr_ae hfg'

Premises used: Filter.EventuallyEq, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Measure.ae_ae_of_ae_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f g : α × β → ℝ≥0∞
hg : Measurable g
hfg : f =ᶠ[ae (μ.prod ν)] g
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) fun (x : α) ↦ ∫⁻ (y : β), g (x, y) ∂ν

Tactic:
exact (ae_ae_of_ae_prod hfg).mono fun x hfg' ↦ lintegral_congr_ae hfg'

Premises used: MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Measure.ae_ae_of_ae_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → β → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f x y ∂ν) μ

Tactic:
hf.lintegral_prod_right'

Premises used: AEMeasurable.lintegral_prod_right'
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : β) ↦ ∫⁻ (x : α), f (x, y) ∂μ) ν

Tactic:
hf.prod_swap.lintegral_prod_right'

Premises used: AEMeasurable.prod_swap, AEMeasurable.lintegral_prod_right', Prod.swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α → β → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (y : β) ↦ ∫⁻ (x : α), f x y ∂μ) ν

Tactic:
hf.lintegral_prod_left'

Premises used: AEMeasurable.lintegral_prod_left'
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (z : α × β), f z ∂μ.prod ν

Tactic:
measurePreserving_swap.lintegral_comp_emb MeasurableEquiv.prodComm.measurableEmbedding f

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.lintegral_comp_emb, MeasurableEquiv.prodComm, MeasureTheory.Measure.measurePreserving_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
rw :
  ∀ (hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)),
    (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
rw [Measure.prod] at *

Premises used: MeasureTheory.Measure.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)
rw : ∫⁻ (a : α), ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
⊢ (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
rw [lintegral_bind Measurable.map_prodMk_left.aemeasurable hf]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.lintegral_bind, Measurable.map_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)
h :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν) fun (a : α) ↦
    ∫⁻ (y : β), f (a, y) ∂ν
⊢ ∫⁻ (a : α), ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)
h :
  ∀ (a : α) (ha : AEMeasurable (_m := Prod.instMeasurableSpace) f (map (Prod.mk a) ν)),
    ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν = ∫⁻ (y : β), f (a, y) ∂ν
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν) fun (a : α) ↦
    ∫⁻ (y : β), f (a, y) ∂ν

Tactic:
filter_upwards [Measurable.map_prodMk_left.aemeasurable.ae_of_bind hf] with a ha

Premises used: Measurable.aemeasurable, AEMeasurable.ae_of_bind, Measurable.map_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)
a : α
ha : AEMeasurable (_m := Prod.instMeasurableSpace) f (map (Prod.mk a) ν)
⊢ AEMeasurable (Prod.mk a) ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable (_m := Prod.instMeasurableSpace) f (μ.bind fun (x : α) ↦ map (Prod.mk x) ν)
a : α
ha : AEMeasurable (_m := Prod.instMeasurableSpace) f (map (Prod.mk a) ν)
⊢ ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν = ∫⁻ (y : β), f (a, y) ∂ν

Tactic:
exact lintegral_map' ha (by fun_prop)

Premises used: MeasureTheory.lintegral_map'
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α × β → ℝ≥0∞
rw : (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
rw [Measure.prod]

Premises used: MeasureTheory.Measure.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α × β → ℝ≥0∞
⊢ (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
(lintegral_bind_le _ _ _).trans <| lintegral_mono fun a ↦ lintegral_map_le _ _

Premises used: Prod.mk, MeasureTheory.Measure.lintegral_bind_le, MeasureTheory.lintegral_mono, MeasureTheory.lintegral_map_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α × β → ℝ≥0∞
⊢ (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ

Tactic:
exact (lintegral_bind_le _ _ _).trans <| lintegral_mono fun a ↦ lintegral_map_le _ _

Premises used: MeasureTheory.Measure.lintegral_bind_le, MeasureTheory.lintegral_mono, MeasureTheory.lintegral_map_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf rwa rwa₁ rwa₂ rwa₃ : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable f ((μ.restrict s).prod (ν.restrict t))

Tactic:
rwa [Measure.prod_restrict]

Premises used: MeasureTheory.Measure.prod_restrict
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
rw : ∫⁻ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
rw₁ rw₂ : ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ

Tactic:
rw [← Measure.prod_restrict, lintegral_prod _ (by rwa [Measure.prod_restrict])]

Premises used: MeasureTheory.Measure.prod_restrict, MeasureTheory.lintegral_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
simp_rw : ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
simp_rw [← lintegral_prod_swap f]

Premises used: MeasureTheory.lintegral_prod_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
lintegral_prod _ hf.prod_swap

Premises used: AEMeasurable.prod_swap, MeasureTheory.lintegral_prod, Prod.swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
exact lintegral_prod _ hf.prod_swap

Premises used: AEMeasurable.prod_swap, MeasureTheory.lintegral_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν

Tactic:
lintegral_prod_symm f hf.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.lintegral_prod_symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
rw : ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : β × α) ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict,
    setLIntegral_prod]

Premises used: MeasureTheory.lintegral_prod_swap, MeasureTheory.Measure.prod_restrict, MeasureTheory.setLIntegral_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : β × α) ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
AEMeasurable.comp_measurable ?_ measurable_swap

Premises used: AEMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
hf₁ : AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)))
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : β × α) ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))

Tactic:
refine AEMeasurable.comp_measurable ?_ measurable_swap

Premises used: AEMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
⊢ AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))

Tactic:
hf
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
h : map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
⊢ AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)))

Tactic:
convert! hf
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
f : α × β → ℝ≥0∞
hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))
h : map Prod.swap ((ν.restrict t).prod (μ.restrict s)) = (μ.prod ν).restrict (s ×ˢ t)
h₁ : (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
h₂ h₃ : (μ.prod ν).restrict (s ×ˢ t) = (μ.prod ν).restrict (s ×ˢ t)
⊢ map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)

Tactic:
rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]

Premises used: MeasureTheory.Measure.prod_swap, MeasureTheory.Measure.prod_restrict
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → β → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : α × β), f z.1 z.2 ∂μ.prod ν

Tactic:
(lintegral_prod _ hf).symm

Premises used: MeasureTheory.lintegral_prod, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α → β → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (z : β × α), f z.2 z.1 ∂ν.prod μ

Tactic:
(lintegral_prod_symm _ hf.prod_swap).symm

Premises used: AEMeasurable.prod_swap, MeasureTheory.lintegral_prod_symm, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
f : α → β → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x y ∂ν ∂μ = ∫⁻ (y : β), ∫⁻ (x : α), f x y ∂μ ∂ν

Tactic:
(lintegral_lintegral hf).trans (lintegral_prod_symm _ hf)

Premises used: MeasureTheory.lintegral_prod_symm, MeasureTheory.lintegral_lintegral, Eq.trans