awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
funProp₂ : inst_2 ≤ inst_2
⊢ Measurable (Prod.map f g)
have funProp₃ : MeasurableEmbedding.{u_3, u_4} (β := ω) fun (a : γ) ↦ g a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 τ υ
⊢ QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)
have refine : map (Prod.map f g) (μ.prod τ) ≪ ν.prod υ
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 τ υ
⊢ Measurable f
have funProp : inst ≤ inst
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Measurable f
have funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := β) fun (a : α) ↦ f a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 τ υ
⊢ Measurable g
have funProp : inst_2 ≤ inst_2
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Measurable g
have funProp₁ : MeasurableEmbedding.{u_3, u_4} (β := ω) fun (a : γ) ↦ g a
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 τ υ
⊢ map (Prod.map f g) (μ.prod τ) ≪ ν.prod υ
have rw : Measure.prod (map f μ) (map g τ) ≪ ν.prod υ
Tactic: rw [← map_prod_map _ _ (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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 (β := γ) (fun (z : α × β) ↦ f z.swap) (μ.prod ν)
have hf₁ : AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap (μ.prod ν))
Tactic: rw [← Measure.prod_swap] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ
have obtain : ∀ (g : α × β → ℝ≥0∞) (hg : Measurable g) (hfg : f =ᶠ[ae (μ.prod ν)] g),
  AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ
Tactic: obtain ⟨g, hg, hfg⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) μ
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), f (x, y) ∂ν) fun (x : α) ↦ ∫⁻ (y : β), g (x, y) ∂ν
Tactic: refine ⟨fun x ↦ ∫⁻ y, g (x, y) ∂ν, by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α × β → ℝ≥0∞
hf : AEMeasurable f (μ.prod ν)
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have 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) ∂ν ∂μ
Tactic: rw [Measure.prod] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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) ν)
⊢ (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have rw : ∫⁻ (a : α), ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
Tactic: rw [lintegral_bind Measurable.map_prodMk_left.aemeasurable hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 : α), ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν) fun (a : α) ↦
  ∫⁻ (y : β), f (a, y) ∂ν
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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) ν)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν) fun (a : α) ↦
    ∫⁻ (y : β), f (a, y) ∂ν
have h : ∀ (a : α) (ha : AEMeasurable (_m := Prod.instMeasurableSpace) f (map (Prod.mk a) ν)),
  ∫⁻ (x : α × β), f x ∂map (Prod.mk a) ν = ∫⁻ (y : β), f (a, y) ∂ν
Tactic: filter_upwards [Measurable.map_prodMk_left.aemeasurable.ae_of_bind hf] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α × β → ℝ≥0∞
⊢ ∫⁻ (z : α × β), f z ∂μ.prod ν ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
have rw : (∫⁻ (z : α × β), f z ∂μ.bind fun (x : α) ↦ map (Prod.mk x) ν) ≤ ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
Tactic: rw [Measure.prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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))
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
have rw : ∫⁻ (z : α × β), f z ∂(μ.restrict s).prod (ν.restrict t) = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
Tactic: rw [← Measure.prod_restrict, lintegral_prod _ (by rwa [Measure.prod_restrict])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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) ∂ν ∂μ
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
have rw₁ : ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ = ∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂ν ∂μ
Tactic: rw [← Measure.prod_restrict, lintegral_prod _ (by rwa [Measure.prod_restrict])]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 ∂μ.prod ν = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
have simp_rw : ∫⁻ (z : β × α), f z.swap ∂ν.prod μ = ∫⁻ (y : β), ∫⁻ (x : α), f (x, y) ∂μ ∂ν
Tactic: simp_rw [← lintegral_prod_swap f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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))
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
have rw : ∫⁻ (x : β) in t, ∫⁻ (y : α) in s, f (x, y).swap ∂μ ∂ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
Tactic: rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict,
    setLIntegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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) ∂μ ∂ν
⊢ ∫⁻ (z : α × β) in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ (y : β) in t, ∫⁻ (x : α) in s, f (x, y) ∂μ ∂ν
have hf₁ : AEMeasurable (β := ℝ≥0∞) (fun (z : β × α) ↦ f z.swap) ((ν.prod μ).restrict (t ×ˢ s))
Tactic: rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict,
    setLIntegral_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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))
have hf₁ : AEMeasurable (_m := Prod.instMeasurableSpace) f (map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)))
Tactic: refine AEMeasurable.comp_measurable ?_ measurable_swap
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 (_m := Prod.instMeasurableSpace) f (map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)))
have h : map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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))
⊢ map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
have h : map Prod.swap ((ν.restrict t).prod (μ.restrict s)) = (μ.prod ν).restrict (s ×ˢ t)
Tactic: rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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)
⊢ map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
have h₁ : (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
Tactic: rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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)
⊢ map Prod.swap ((ν.prod μ).restrict (t ×ˢ s)) = (μ.prod ν).restrict (s ×ˢ t)
have h₂ : (μ.prod ν).restrict (s ×ˢ t) = (μ.prod ν).restrict (s ×ˢ t)
Tactic: rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp : inst ≤ inst
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp₂ : map (fun (a : α × β) ↦ a.1) (μ.prod ν) ≪ μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
funProp₂ : map (fun (a : α × β) ↦ a.1) (μ.prod ν) ≪ μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp₃ : inst_1 ≤ inst_1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
funProp₂ : map (fun (a : α × β) ↦ a.1) (μ.prod ν) ≪ μ
funProp₃ : inst_1 ≤ inst_1
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : β) ↦ g a0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : α) ↦ f a0
funProp₂ : map (fun (a : α × β) ↦ a.1) (μ.prod ν) ≪ μ
funProp₃ : inst_1 ≤ inst_1
funProp₄ : MeasurableEmbedding (β := ℝ≥0∞) fun (a0 : β) ↦ g a0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (z : α × β) ↦ f z.1 * g z.2) (μ.prod ν)
have funProp₅ : map (fun (a : α × β) ↦ a.2) (μ.prod ν) ≪ ν
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
have rw : ∫⁻ (x : α), ∫⁻ (y : β), f (x, y).1 * g (x, y).2 ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
Tactic: rw [lintegral_prod _ (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((map Prod.fst ρ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
Tactic: rw [fst, Measure.map_apply measurable_fst hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map Prod.fst ρ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
  ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
Tactic: rw [fst, Measure.map_apply measurable_fst hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' univ) : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [fst_apply MeasurableSet.univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
rw :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' univ) : ℝ≥0∞)
    ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [fst_apply MeasurableSet.univ, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: rw [fst_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.fst
have inl : ∀ (h : ρ = 0), IsZeroOrProbabilityMeasure ρ.fst
Tactic: rcases eq_zero_or_isProbabilityMeasure ρ with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
inl : ∀ (h : ρ = 0), IsZeroOrProbabilityMeasure ρ.fst
⊢ IsZeroOrProbabilityMeasure ρ.fst
have inr : ∀ (h : IsProbabilityMeasure ρ), IsZeroOrProbabilityMeasure ρ.fst
Tactic: rcases eq_zero_or_isProbabilityMeasure ρ with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
ρ : Measure (α × β)
inst_4 : IsZeroOrProbabilityMeasure ρ
h : ρ = 0
⊢ IsZeroOrProbabilityMeasure ρ.fst
have inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := inst) 0
Tactic: simp only [h, fst_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
⊢ (μ.prod ν).fst = μ
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
s : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((μ.prod ν).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]