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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst_4 : SFinite μa
inst_5 : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
⊢ Eq (α := Measure (β × δ)) (Measure.prod (map f (sfiniteSeq μa i.1)) (map g (sfiniteSeq μc i.2)))
    (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)))
have e_f : ∀ (s : Set β) (t : Set δ) (hs : MeasurableSet s) (ht : MeasurableSet t),
  (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map f (sfiniteSeq μa i.1) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((map g (sfiniteSeq μc i.2) : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine prod_eq fun s t hs ht => ?_
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
f : α → β
g : γ → δ
μa : Measure α
μc : Measure γ
inst_4 : SFinite μa
inst_5 : SFinite μc
hf : Measurable f
hg : Measurable g
i : ℕ × ℕ
s : Set β
t : Set δ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map (Prod.map f g) ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2)) : (a : Set (β × δ)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((map f (sfiniteSeq μa i.1) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((map g (sfiniteSeq μc i.2) : Measure δ) : (a : Set δ) → ℝ≥0∞) t : ℝ≥0∞)
have e_f : ((sfiniteSeq μa i.1).prod (sfiniteSeq μc i.2) : (a : Set (α × γ)) → ℝ≥0∞) (Prod.map f g ⁻¹' s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μa i.1 : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((sfiniteSeq μc i.2 : (a : Set γ) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: rw [map_apply (hf.prodMap hg) (hs.prod ht), map_apply hf hs, map_apply hg ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
μ : Measure α
c : ℝ≥0∞
⊢ (c • μ).prod ν = c • μ.prod ν
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((c • μ).prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext 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 β
inst_2 : SFinite ν
μ : Measure α
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((c • μ).prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂c • μ =
  c • ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
Tactic: rw [prod_apply hs, Measure.smul_apply, prod_apply hs]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
⊢ MeasurePreserving (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)
have this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
Tactic: have : Measurable fun p : α × γ => (f p.1, g p.1 p.2) := (hf.1.comp measurable_fst).prodMk hgm
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
⊢ MeasurePreserving (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)
have map_eq : map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
Tactic: use this
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
⊢ map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
have map_eq : ∀ [SFinite.{u_1} (α := α) (m0 := inst) 0] (hf : MeasurePreserving f 0 μb) (hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd),
  map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd
Tactic: rcases eq_zero_or_neZero μa with rfl | _
Cleared hypotheses: μa, inst_4, hf, hg
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
map_eq :
  ∀ [SFinite.{u_1} (α := α) (m0 := inst) 0] (hf : MeasurePreserving f 0 μb) (hg : ∀ᵐ (a : α) ∂0, map (g a) μc = μd),
    map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (Measure.prod 0 μc) = μb.prod μd
⊢ map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
have map_eq₁ : NeZero μa → map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
Tactic: rcases eq_zero_or_neZero μa with rfl | _
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
⊢ SFinite μd
have obtain : ∀ (a : α) (ha : map (g a) μc = μd), SFinite μd
Tactic: obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
a : α
ha : map (g a) μc = μd
⊢ SFinite μd
have rw : SFinite (m0 := inst_3) (map (g a) μc)
Tactic: rw [← ha]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
⊢ map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
have sf : SFinite μd
Tactic: have sf : SFinite μd := by
    obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
    rw [← ha]
    infer_instance
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
sf : SFinite μd
⊢ map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
have map_eq : ∀ (s : Set (β × δ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μb.prod μd : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μb.prod μd : (a : Set (β × δ)) → ℝ≥0∞) s : ℝ≥0∞)
have map_eq : ∫⁻ (x : α), (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) ∂μa =
  ∫⁻ (a : α), (μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) ∂μa
Tactic: rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs,
    ← hf.lintegral_comp (measurable_measure_prodMk_left hs)]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk x ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) ∂μa =
    ∫⁻ (a : α), (μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) ∂μa
have map_eq : (ae μa).EventuallyEq (β := ℝ≥0∞)
  (fun (a : α) ↦ (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s)) fun (a : α) ↦
  (μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s)
Tactic: apply lintegral_congr_ae
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
⊢ (ae μa).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s)) fun (a : α) ↦
    (μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s)
have h : ∀ (a : α) (ha : map (g a) μc = μd),
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
Tactic: filter_upwards [hg] with a ha
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
⊢ Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
  (((map (g a) μc : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h_1 : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
h :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    (((map (g a) μc : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
  ((μc : (a : Set γ) → ℝ≥0∞) (g a ⁻¹' Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h_1 : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
h :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    (((map (g a) μc : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μc : (a : Set γ) → ℝ≥0∞) (g a ⁻¹' Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) : ℝ≥0∞)
  ((μc : (a : Set γ) → ℝ≥0∞) (g a ⁻¹' Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]
-- 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 γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μa
inst_5 : SFinite μc
f : α → β
hf : MeasurePreserving f μa μb
g : α → γ → δ
hgm : Measurable (uncurry g)
hg : ∀ᵐ (a : α) ∂μa, map (g a) μc = μd
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
h_1 : NeZero μa
sf : SFinite μd
s : Set (β × δ)
hs : MeasurableSet s
a : α
ha : map (g a) μc = μd
h :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    (((map (g a) μc : Measure δ) : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μc : (a : Set γ) → ℝ≥0∞) (g a ⁻¹' Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) : ℝ≥0∞)
    ((μc : (a : Set γ) → ℝ≥0∞) (g a ⁻¹' Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) (Prod.mk a ⁻¹' (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) ⁻¹' s) : ℝ≥0∞)
    ((μd : (a : Set δ) → ℝ≥0∞) (Prod.mk (f a) ⁻¹' s) : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μc : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (f (a, x).1, g (a, x).1 (a, x).2)) ⁻¹' s) : ℝ≥0∞)
  ((μc : (a : Set γ) → ℝ≥0∞) ((fun (x : γ) ↦ (f a, g a x)) ⁻¹' s) : ℝ≥0∞)
Tactic: rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ
have refine : map f (μ.prod ν) ≪ τ
Tactic: refine ⟨hf, ?_⟩
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
⊢ map f (μ.prod ν) ≪ τ
have refine : ∀ (s : Set γ) (hs : MeasurableSet s) (h2s : Eq (α := ℝ≥0∞) ((τ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (((map f (μ.prod ν) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs h2s => ?_
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((τ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f (μ.prod ν) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f ⁻¹' s) ∂μ = 0
Tactic: rw [map_apply hf hs, Measure.prod_apply (hf hs)]
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((τ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f ⁻¹' s) ∂μ = 0
have simp_rw : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) ((fun (x_1 : β) ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0
Tactic: simp_rw [preimage_preimage]
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((τ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) ((fun (x_1 : β) ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0
have rw : ∫⁻ (a : α), 0 ∂μ = 0
Tactic: rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]
-- 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 γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite ν
h2f : ∀ᵐ (x : α) ∂μ, QuasiMeasurePreserving (fun (y : β) ↦ f (x, y)) ν τ
s : Set γ
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((τ : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : ∫⁻ (a : α), 0 ∂μ = 0
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) ((fun (x_1 : β) ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α × β → γ
μ : Measure α
ν : Measure β
τ : Measure γ
hf : Measurable f
inst_3 : SFinite μ
inst_4 : SFinite ν
h2f : ∀ᵐ (y : β) ∂ν, QuasiMeasurePreserving (fun (x : α) ↦ f (x, y)) μ τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ
have rw : QuasiMeasurePreserving (m0 := Prod.instMeasurableSpace) f (map Prod.swap (ν.prod μ)) τ
Tactic: rw [← prod_swap]
-- 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 (Prod.map f g)
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 (Prod.map f g)
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 τ υ
funProp : inst ≤ inst
funProp₁ : MeasurableEmbedding.{u_1, u_2} (β := β) fun (a : α) ↦ f a
⊢ Measurable (Prod.map f g)
have funProp₂ : inst_2 ≤ inst_2
Tactic: fun_prop