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 γ
δ : 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
⊢ ((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:
prod_prod (f ⁻¹' s) (g ⁻¹' t)

Premises used: Set.Mem, setOf, Set.prod, MeasureTheory.Measure.prod_prod, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ ((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:
exact prod_prod (f ⁻¹' s) (g ⁻¹' t)

Premises used: MeasureTheory.Measure.prod_prod, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
μ : Measure α
c : ℝ≥0∞
h :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((c • μ).prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
      ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (c • μ).prod ν = c • μ.prod ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
μ : Measure α
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
h :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂c • μ =
    c • ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
⊢ Eq (α := ℝ≥0∞) (((c • μ).prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((c • μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [prod_apply hs, Measure.smul_apply, prod_apply hs]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
μ : Measure α
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂c • μ =
    c • ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
⊢ MeasurePreserving (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Tactic:
use this
-- Module: Mathlib.MeasureTheory.Measure.Prod
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_eq₁ : NeZero μa → map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd
⊢ 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 | _

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
δ : Type u_4
inst_3 : MeasurableSpace δ
μb : Measure β
μc : Measure γ
μd : Measure δ
inst_4 : SFinite μc
f : α → β
g : α → γ → δ
hgm : Measurable (uncurry g)
this : Measurable (β := β × δ) fun (p : α × γ) ↦ (f p.1, g p.1 p.2)
inst_5 : 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:
simp [← hf.map_eq]

Premises used: MeasureTheory.MeasurePreserving.map_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α), map (g a) μc = μd

Tactic:
hg.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
obtain : ∀ (a : α) (ha : map (g a) μc = μd), SFinite μd
⊢ SFinite μd

Tactic:
obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw : SFinite (m0 := inst_3) (map (g a) μc)
⊢ SFinite μd

Tactic:
rw [← ha]
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 (m0 := inst_3) (map (g a) μc)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
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

Tactic:
have sf : SFinite μd := by
    obtain ⟨a, ha⟩ : ∃ a, map (g a) μc = μd := hg.exists
    rw [← ha]
    infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
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_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∞)
⊢ map (fun (p : α × γ) ↦ (f p.1, g p.1 p.2)) (μa.prod μc) = μb.prod μd

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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
⊢ 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:
rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs,
    ← hf.lintegral_comp (measurable_measure_prodMk_left hs)]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_apply, measurable_measure_prodMk_left, MeasureTheory.MeasurePreserving.lintegral_comp
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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)
⊢ ∫⁻ (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:
apply lintegral_congr_ae

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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∞)
⊢ (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:
filter_upwards [hg] with a ha
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
h₃ 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∞)
⊢ 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:
rw [← ha, map_apply hgm.of_uncurry_left (measurable_prodMk_left hs), preimage_preimage,
    preimage_preimage]

Premises used: Set.preimage_preimage, MeasureTheory.Measure.map_apply, Measurable.of_uncurry_left, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α → β
g : γ → δ
hf : MeasurePreserving f μa μb
hg : MeasurePreserving g μc μd
⊢ MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)

Tactic:
have : Measurable (uncurry fun _ : α => g) := hg.1.comp measurable_snd
  hf.skew_product this <| ae_of_all _ fun _ => hg.map_eq

Premises used: Measurable.comp, Prod.map, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.ae_of_all, measurable_snd, MeasureTheory.MeasurePreserving.measurable, MeasureTheory.MeasurePreserving.skew_product
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν) τ

Tactic:
⟨hf, ?_⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)) ν τ
refine : map f (μ.prod ν) ≪ τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
refine ⟨hf, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν) ≪ τ

Tactic:
AbsolutelyContinuous.mk fun s hs h2s => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)) ν τ
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∞)
⊢ map f (μ.prod ν) ≪ τ

Tactic:
refine AbsolutelyContinuous.mk fun s hs h2s => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f ⁻¹' s) ∂μ = 0
⊢ Eq (α := ℝ≥0∞) (((map f (μ.prod ν) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply hf hs, Measure.prod_apply (hf hs)]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_apply
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
simp_rw : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) ((fun (x_1 : β) ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' f ⁻¹' s) ∂μ = 0

Tactic:
simp_rw [preimage_preimage]

Premises used: Set.preimage_preimage
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) ((fun (x_1 : β) ↦ f (x, x_1)) ⁻¹' s) ∂μ = 0

Tactic:
rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero]

Premises used: MeasureTheory.lintegral_zero, MeasureTheory.lintegral_congr_ae, Filter.Eventually.mono, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)) μ τ
rw : QuasiMeasurePreserving (m0 := Prod.instMeasurableSpace) f (map Prod.swap (ν.prod μ)) τ
⊢ QuasiMeasurePreserving f (μ.prod ν) τ

Tactic:
rw [← prod_swap]

Premises used: MeasureTheory.Measure.prod_swap
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 (m0 := Prod.instMeasurableSpace)
    ((f ∘ Prod.swap) ∘ (⇑(MeasurableEquiv.symm MeasurableEquiv.prodComm) : (a : α × β) → β × α))
    (map Prod.swap (ν.prod μ)) τ

Tactic:
(QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
      ((measurable_swap.measurePreserving (ν.prod μ)).symm
          MeasurableEquiv.prodComm).quasiMeasurePreserving

Premises used: Measurable.comp, MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasureTheory.QuasiMeasurePreserving.prod_of_right, MeasureTheory.Measure.QuasiMeasurePreserving.comp, measurable_swap, MeasureTheory.Measure.prod, MeasurableEquiv.prodComm, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 (m0 := Prod.instMeasurableSpace) f (map Prod.swap (ν.prod μ)) τ

Tactic:
convert!
    (QuasiMeasurePreserving.prod_of_right (hf.comp measurable_swap) h2f).comp
      ((measurable_swap.measurePreserving (ν.prod μ)).symm
          MeasurableEquiv.prodComm).quasiMeasurePreserving

Premises used: Measurable.comp, MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasureTheory.QuasiMeasurePreserving.prod_of_right, MeasureTheory.Measure.QuasiMeasurePreserving.comp, measurable_swap, MeasureTheory.Measure.prod, MeasurableEquiv.prodComm, MeasureTheory.MeasurePreserving.quasiMeasurePreserving
-- 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 γ
f : α → β × γ
hf : QuasiMeasurePreserving f μ (ν.prod τ)
⊢ QuasiMeasurePreserving (fun (x : α) ↦ (f x).1) μ ν

Tactic:
(quasiMeasurePreserving_fst (μ := ν) (ν := τ)).comp hf

Premises used: MeasureTheory.Measure.quasiMeasurePreserving_fst, MeasureTheory.Measure.QuasiMeasurePreserving.comp
-- 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 γ
f : α → β × γ
hf : QuasiMeasurePreserving f μ (ν.prod τ)
⊢ QuasiMeasurePreserving (fun (x : α) ↦ (f x).2) μ τ

Tactic:
(quasiMeasurePreserving_snd (μ := ν) (ν := τ)).comp hf

Premises used: MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.comp
-- 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
funProp₂ : inst_2 ≤ inst_2
funProp₃ : MeasurableEmbedding.{u_3, u_4} (β := ω) fun (a : γ) ↦ g a
⊢ Measurable (Prod.map f g)

Tactic:
fun_prop