awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t : Set (α × β)) (hst : s ⊆ t) (mt : MeasurableSet t)
    (ht : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0

Tactic:
obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h

Premises used: mt, MeasureTheory.exists_measurable_superset_of_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' t)) 0

Tactic:
rw [measure_prod_null mt] at ht

Premises used: MeasureTheory.Measure.measure_prod_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' t)) 0
rw :
  (ae μ).EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0 ∧
    (ae μ).EventuallyLE (β := ℝ≥0∞) 0 fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0

Tactic:
rw [eventuallyLE_antisymm_iff]

Premises used: Filter.eventuallyLE_antisymm_iff
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' t)) 0
⊢ (ae μ).EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0 ∧
    (ae μ).EventuallyLE (β := ℝ≥0∞) 0 fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht,
      Eventually.of_forall fun x => zero_le⟩

Premises used: zero_le, Filter.EventuallyLE.trans_eq, Filter.Eventually.of_forall, Set.preimage_mono, And.intro, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set (α × β)
hst : s ⊆ t
mt : MeasurableSet t
ht : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' t)) 0
⊢ (ae μ).EventuallyLE (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0 ∧
    (ae μ).EventuallyLE (β := ℝ≥0∞) 0 fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)

Tactic:
exact
    ⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht,
      Eventually.of_forall fun x => zero_le⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
⊢ μ.prod ν ≪ μ'.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
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
refine :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s)
    (h2s : Eq (α := ℝ≥0∞) ((μ'.prod ν' : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.prod ν ≪ μ'.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
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ'.prod ν' : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
apply : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_prod_null_of_ae_null hs

Premises used: MeasureTheory.Measure.measure_prod_null_of_ae_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ'.prod ν' : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ').EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0

Tactic:
rw [measure_prod_null hs] at h2s

Premises used: MeasureTheory.Measure.measure_prod_null
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (ae μ').EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0

Tactic:
(h2s.filter_mono h1.ae_le).mono fun _ h => h2 h

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq, Filter.Eventually.mono, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst_2 : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (ae μ').EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0

Tactic:
exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h

Premises used: Filter.EventuallyEq.filter_mono, Filter.Eventually.mono, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
p : α × β → Prop
h : ∀ᵐ (z : α × β) ∂μ.prod ν, p z
⊢ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)

Tactic:
measure_ae_null_of_prod_null h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasureTheory.Measure.measure_ae_null_of_prod_null, Set.preimage, Not
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
γ : Type u_4
f g : α × β → γ
h : f =ᶠ[ae (μ.prod ν)] g
⊢ ∀ᵐ (x : α) ∂μ, Function.curry f x =ᶠ[ae ν] Function.curry g x

Tactic:
ae_ae_of_ae_prod h

Premises used: Filter.EventuallyEq, 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 ν
γ : Type u_4
f g : α → β → γ
h : uncurry f =ᶠ[ae (μ.prod ν)] uncurry g
⊢ ∀ᵐ (x : α) ∂μ, f x =ᶠ[ae ν] g x

Tactic:
ae_ae_eq_curry_of_prod h

Premises used: MeasureTheory.Measure.ae_ae_eq_curry_of_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
p : α × β → Prop
hp : MeasurableSet (α := α × β) {x : α × β | p x}
⊢ (∀ᵐ (z : α × β) ∂μ.prod ν, p z) ↔ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, p (x, y)

Tactic:
measure_prod_null hp.compl

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasurableSet.compl, Set.preimage, MeasureTheory.Measure.measure_prod_null, Not
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ (∀ᵐ (z : α × β) ∂μ.prod ν, z ∈ s) ↔ ∀ᵐ (x : α) ∂μ, ∀ᵐ (y : β) ∂ν, (x, y) ∈ s

Tactic:
measure_prod_null hs.compl

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasurableSet.compl, Set.preimage, MeasureTheory.Measure.measure_prod_null, Not
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk, MeasureTheory.Measure.QuasiMeasurePreserving.mk, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (h2s : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((map Prod.fst (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ

Tactic:
refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map Prod.fst (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]

Premises used: MeasureTheory.Measure.map_apply, Set.prod_univ, measurable_fst, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(prod_prod_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Measure.prod_prod_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine (prod_prod_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Measure.prod_prod_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0

Tactic:
rw [h2s, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.snd (μ.prod ν) ν

Tactic:
⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk, MeasureTheory.Measure.QuasiMeasurePreserving.mk, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
refine :
  ∀ (s : Set β) (hs : MeasurableSet s) (h2s : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) (((map Prod.snd (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ QuasiMeasurePreserving Prod.snd (μ.prod ν) ν

Tactic:
refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map Prod.snd (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [map_apply measurable_snd hs, ← univ_prod, ← nonpos_iff_eq_zero]

Premises used: MeasureTheory.Measure.map_apply, Set.univ_prod, measurable_snd, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(prod_prod_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Measure.prod_prod_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = 0
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine (prod_prod_le _ _).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.Measure.prod_prod_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = 0

Tactic:
rw [h2s, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s s' : Set α
t t' : Set β
hs : s =ᶠ[ae μ] s'
ht : t =ᶠ[ae ν] t'
⊢ s ×ˢ t =ᶠ[ae (μ.prod ν)] s' ×ˢ t'

Tactic:
(quasiMeasurePreserving_fst.preimage_ae_eq hs).inter
    (quasiMeasurePreserving_snd.preimage_ae_eq ht)

Premises used: Set.Mem, setOf, Set.prod, Filter.EventuallyEq.inter, MeasureTheory.Measure.quasiMeasurePreserving_fst, MeasureTheory.Measure.quasiMeasurePreserving_snd, MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq, Set.preimage
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
s_ae_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t_ae_univ : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) sᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Set.compl_prod_eq_union, measure_union_null_iff]

Premises used: MeasureTheory.measure_union_null_iff, Set.compl_prod_eq_union
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
s_ae_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t_ae_univ : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) sᶜ univ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [s_ae_univ, t_ae_univ]
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
t : Set β
s_mble : NullMeasurableSet s μ
t_mble : NullMeasurableSet t ν
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν)

Tactic:
let ⟨s₀, mble_s₀, s_aeeq_s₀⟩ := s_mble
  let ⟨t₀, mble_t₀, t_aeeq_t₀⟩ := t_mble
  ⟨s₀ ×ˢ t₀, ⟨mble_s₀.prod mble_t₀, set_prod_ae_eq s_aeeq_s₀ t_aeeq_t₀⟩⟩

Premises used: SProd.sprod, MeasureTheory.NullMeasurableSet, MeasurableSet.prod, MeasureTheory.Measure.prod, MeasureTheory.Measure.set_prod_ae_eq, And.intro, _private.0.MeasureTheory.NullMeasurableSet.prod.match_1, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rcases : ∀ (u : Set (α × β)) (hum : MeasurableSet u) (hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u), NullMeasurableSet t ν
⊢ NullMeasurableSet t ν

Tactic:
rcases h with ⟨u, hum, hu⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
⊢ ∃ x ∈ s, Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u

Tactic:
((frequently_ae_iff.2 hs).and_eventually (ae_ae_eq_curry_of_prod hu)).exists

Premises used: Iff.mpr, Set.Mem, setOf, Set.prod, MeasureTheory.Measure.ae_ae_eq_curry_of_prod, Filter.Frequently.and_eventually, Set.preimage, Filter.Frequently.exists, MeasureTheory.frequently_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
obtain : ∀ (x : α) (hxs : x ∈ s) (hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u), NullMeasurableSet t ν
⊢ NullMeasurableSet t ν

Tactic:
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, (Prod.mk x ⁻¹' (s ×ˢ t)) =ᵐ[ν] (Prod.mk x ⁻¹' u) :=
    ((frequently_ae_iff.2 hs).and_eventually (ae_ae_eq_curry_of_prod hu)).exists

Premises used: Iff.mpr, MeasureTheory.Measure.ae_ae_eq_curry_of_prod, Filter.Frequently.and_eventually, Filter.Frequently.exists, MeasureTheory.frequently_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν

Tactic:
⟨Prod.mk x ⁻¹' u, measurable_prodMk_left hum, ?_⟩

Premises used: MeasurableSet, MeasureTheory.NullMeasurableSet, Prod.mk, Set.preimage, And.intro, Exists.intro, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
refine : t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν

Tactic:
refine ⟨Prod.mk x ⁻¹' u, measurable_prodMk_left hum, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : t =ᶠ[ae ν] Prod.mk x ⁻¹' u), t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u

Tactic:
rwa [mk_preimage_prod_right hxs] at hx

Premises used: Set.mk_preimage_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 : NeZero μ
t : Set β
h : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
rwa rwa₁ rwa₂ rwa₃ : NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν)
⊢ NullMeasurableSet (SProd.sprod (α := Set α) univ t) (μ.prod ν)

Tactic:
rwa [univ_prod]

Premises used: Set.univ_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 : NeZero μ
t : Set β
⊢ NullMeasurableSet (Prod.snd ⁻¹' t) (μ.prod ν) ↔ NullMeasurableSet t ν

Tactic:
⟨.of_preimage_snd, (.preimage · quasiMeasurePreserving_snd)⟩

Premises used: MeasureTheory.NullMeasurableSet.of_preimage_snd, MeasureTheory.NullMeasurableSet.preimage, MeasureTheory.Measure.quasiMeasurePreserving_snd, Iff.intro
-- 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 : NeZero μ
f : β → γ
⊢ NullMeasurable (f ∘ Prod.snd) (μ.prod ν) ↔ NullMeasurable f ν

Tactic:
forall₂_congr fun s _ ↦ nullMeasurableSet_preimage_snd (t := f ⁻¹' s)

Premises used: forall₂_congr, MeasureTheory.Measure.nullMeasurableSet_preimage_snd, MeasureTheory.NullMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
⊢ SigmaFinite ν

Tactic:
haveI := hν.sigmaFinite