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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
ν₁ :
  LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (S ×ˢ T) : ℝ≥0∞)
ν₂ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' S ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
ν₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
calc
    μ.prod ν (s ×ˢ t) ≤ μ.prod ν (S ×ˢ T) := by gcongr <;> apply subset_toMeasurable
    _ ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' (S ×ˢ T)) ∂μ := prod_apply_le (by measurability)
    _ = μ S * ν T := by
      classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, mul_comm]
    _ = μ s * ν t := by rw [measure_toMeasurable, measure_toMeasurable]

Premises used: SProd.sprod, MeasureTheory.Measure.prod_apply_le, MeasureTheory.Measure.prod, DFunLike.coe
-- 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 γ
inst_3 : NoAtoms μ
x : α
y : β
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) {x} {y}) : ℝ≥0∞)

Tactic:
rw [singleton_prod_singleton]

Premises used: Set.singleton_prod_singleton
-- 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 γ
inst_3 : NoAtoms μ
x : α
y : β
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) {y} : ℝ≥0∞) = 0

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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : NoAtoms ν
x : α
y : β
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) {x} {y}) : ℝ≥0∞)

Tactic:
rw [singleton_prod_singleton]

Premises used: Set.singleton_prod_singleton
-- 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 γ
inst_3 : NoAtoms ν
x : α
y : β
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) {y} : ℝ≥0∞) = 0

Tactic:
simp
-- 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
simp_rw :
  (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (a : Set (α × β)) → ℝ≥0∞) s =
    ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
simp_rw₁ :
  ∫⁻ (a : α), (map (Prod.mk a) ν : (a : Set (α × β)) → ℝ≥0∞) s ∂μ =
    ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s = ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
simp_rw [Measure.prod, bind_apply hs (Measurable.map_prodMk_left (ν := ν)).aemeasurable,
    map_apply measurable_prodMk_left hs]

Premises used: MeasureTheory.Measure.bind_apply, Measurable.aemeasurable, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod, Measurable.map_prodMk_left, 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 β
apply :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
apply (prod_prod_le s t).antisymm

Premises used: MeasureTheory.Measure.prod_prod_le, LE.le.antisymm
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
⊢ MeasurableSet ST

Tactic:
have hSTm : MeasurableSet ST := measurableSet_toMeasurable _ _
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
⊢ s ×ˢ t ⊆ ST

Tactic:
have hST : s ×ˢ t ⊆ ST := subset_toMeasurable _ _
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
⊢ Measurable f

Tactic:
have hfm : Measurable f := measurable_measure_prodMk_left hSTm
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
⊢ s ⊆ s'

Tactic:
have hss' : s ⊆ s' := fun x hx => measure_mono fun y hy => hST <| mk_mem_prod hx hy
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
gcongr
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
    ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) t ∂μ

Tactic:
rw [setLIntegral_const, mul_comm]

Premises used: MeasureTheory.setLIntegral_const, mul_comm
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
⊢ ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) t ∂μ ≤ ∫⁻ (x : α) in s', f x ∂μ

Tactic:
setLIntegral_mono hfm fun x => id

Premises used: id, MeasureTheory.setLIntegral_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 α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
⊢ ∫⁻ (x : α) in s', f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
lintegral_mono' restrict_le_self le_rfl

Premises used: le_rfl, MeasureTheory.lintegral_mono', MeasureTheory.Measure.restrict_le_self
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
⊢ ∫⁻ (x : α), f x ∂μ = (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ST

Tactic:
(prod_apply hSTm).symm

Premises used: MeasureTheory.Measure.prod_apply, Eq.symm
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ST : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)

Tactic:
measure_toMeasurable _

Premises used: MeasureTheory.measure_toMeasurable
-- 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 β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
hST : s ×ˢ t ⊆ ST
f : α → ℝ≥0∞ := fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' ST)
hfm : Measurable f
s' : Set α := {x : α | (ν : (a : Set β) → ℝ≥0∞) t ≤ f x}
hss' : s ⊆ s'
μ₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
μ₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
    ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) t ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)

Tactic:
calc
    μ s * ν t ≤ μ s' * ν t := by gcongr
    _ = ∫⁻ _ in s', ν t ∂μ := by rw [setLIntegral_const, mul_comm]
    _ ≤ ∫⁻ x in s', f x ∂μ := setLIntegral_mono hfm fun x => id
    _ ≤ ∫⁻ x, f x ∂μ := lintegral_mono' restrict_le_self le_rfl
    _ = μ.prod ν ST := (prod_apply hSTm).symm
    _ = μ.prod ν (s ×ˢ t) := measure_toMeasurable _

Premises used: le_rfl, SProd.sprod, MeasureTheory.Measure.prod_apply, id, MeasureTheory.setLIntegral_mono, MeasureTheory.measure_toMeasurable, MeasureTheory.lintegral_mono', MeasureTheory.Measure.prod, MeasureTheory.Measure.restrict_le_self, Eq.symm, DFunLike.coe
-- 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 β
⊢ (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t

Tactic:
simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]

Premises used: MeasureTheory.Measure.prod_prod, ENNReal.toReal_mul, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map Prod.fst (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map Prod.fst (μ.prod ν) = HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ

Tactic:
ext s hs
-- 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
⊢ Eq (α := ℝ≥0∞) (((map Prod.fst (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Measure.map_apply measurable_fst hs, ← prod_univ, mul_comm]

Premises used: MeasureTheory.Measure.map_apply, Set.prod_univ, mul_comm, measurable_fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
rw : HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ = μ
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
rw₂ rw₃ : μ = μ
⊢ map Prod.fst (μ.prod ν) = μ

Tactic:
rw [map_fst_prod, measure_univ, one_smul]

Premises used: MeasureTheory.Measure.map_fst_prod, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((map Prod.snd (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map Prod.snd (μ.prod ν) = HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν

Tactic:
ext s hs
-- 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
⊢ Eq (α := ℝ≥0∞) (((map Prod.snd (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [Measure.map_apply measurable_snd hs, ← univ_prod]

Premises used: MeasureTheory.Measure.map_apply, Set.univ_prod, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
rw : HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν = ν
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 ν = ν
rw₂ rw₃ : ν = ν
⊢ map Prod.snd (μ.prod ν) = ν

Tactic:
rw [map_snd_prod, measure_univ, one_smul]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul, MeasureTheory.Measure.map_snd_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
open_pos :
  ∀ (U : Set (X × Y)),
    IsOpen[instTopologicalSpaceProd] U →
      U.Nonempty → Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ.prod ν).IsOpenPosMeasure

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
open_pos :
  ∀ (u : Set X) (v : Set Y) (u_open : IsOpen[inst_4] u) (v_open : IsOpen[inst_5] v) (xu : x ∈ u) (yv : y ∈ v)
    (huv : u ×ˢ v ⊆ U), Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases isOpen_prod_iff.1 U_open x y hxy with ⟨u, v, u_open, v_open, xu, yv, huv⟩

Premises used: isOpen_prod_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ne_of_gt (lt_of_lt_of_le ?_ (measure_mono huv))

Premises used: ne_of_gt, MeasureTheory.measure_mono, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (u ×ˢ v) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono huv))

Premises used: ne_of_gt, MeasureTheory.measure_mono, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
open_pos :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (u ×ˢ v) : ℝ≥0∞)

Tactic:
simp only [prod_prod, CanonicallyOrderedAdd.mul_pos]

Premises used: MeasureTheory.Measure.prod_prod, CanonicallyOrderedAdd.mul_pos
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞)
open_pos₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
u_open.measure_pos μ ⟨x, xu⟩

Premises used: IsOpen.measure_pos, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst_6 : μ.IsOpenPosMeasure
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : ν.IsOpenPosMeasure
inst_8 : SFinite ν
U : Set (X × Y)
U_open : IsOpen[instTopologicalSpaceProd] U
x : X
y : Y
hxy : (x, y) ∈ U
u : Set X
v : Set Y
u_open : IsOpen[inst_4] u
v_open : IsOpen[inst_5] v
xu : x ∈ u
yv : y ∈ v
huv : u ×ˢ v ⊆ U
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
exact u_open.measure_pos μ ⟨x, xu⟩

Premises used: IsOpen.measure_pos, Exists.intro