awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
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∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
    ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) t ∂μ
have 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∞)
Tactic: rw [setLIntegral_const, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
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∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have μ₁ : 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: 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
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∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have μ₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
  ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) 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 _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
⊢ map Prod.fst (μ.prod ν) = HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ
have 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∞)
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 α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
⊢ map Prod.fst (μ.prod ν) = μ
have rw : HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ = μ
Tactic: rw [map_fst_prod, measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
rw : HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ = μ
⊢ map Prod.fst (μ.prod ν) = μ
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
Tactic: rw [map_fst_prod, measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure ν
rw : HSMul.hSMul (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) μ = μ
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 μ = μ
⊢ map Prod.fst (μ.prod ν) = μ
have rw₂ : μ = μ
Tactic: rw [map_fst_prod, measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
⊢ map Prod.snd (μ.prod ν) = HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν
have 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∞)
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 α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
⊢ map Prod.snd (μ.prod ν) = ν
have rw : HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν = ν
Tactic: rw [map_snd_prod, measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
rw : HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν = ν
⊢ map Prod.snd (μ.prod ν) = ν
have rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 ν = ν
Tactic: rw [map_snd_prod, measure_univ, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : IsProbabilityMeasure μ
rw : HSMul.hSMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ν = ν
rw₁ : HSMul.hSMul (α := ℝ≥0∞) 1 ν = ν
⊢ map Prod.snd (μ.prod ν) = ν
have rw₂ : ν = ν
Tactic: rw [map_snd_prod, measure_univ, one_smul]
-- 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 γ
μ_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 ν
⊢ (μ.prod ν).IsOpenPosMeasure
have open_pos : ∀ (U : Set (X × Y)),
  IsOpen[instTopologicalSpaceProd] U →
    U.Nonempty → Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- 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 γ
μ_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
⊢ Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rcases isOpen_prod_iff.1 U_open x y hxy with ⟨u, v, u_open, v_open, xu, yv, huv⟩
-- 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 γ
μ_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∞)
have open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (u ×ˢ v) : ℝ≥0∞)
Tactic: refine ne_of_gt (lt_of_lt_of_le ?_ (measure_mono huv))
-- 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 γ
μ_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∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (u ×ˢ v) : ℝ≥0∞)
have open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞) ∧
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: simp only [prod_prod, CanonicallyOrderedAdd.mul_pos]
-- 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 γ
μ_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∞) ∧
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
have open_pos : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: constructor
-- 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 γ
μ_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 X) → ℝ≥0∞) u : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
have open_pos₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
hμ : μ.FiniteAtFilter l
hν : ν.FiniteAtFilter l'
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')
have rcases : ∀ (s : Set X) (hs : s ∈ l) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (μ.prod ν).FiniteAtFilter (l ×ˢ l')
Tactic: rcases hμ with ⟨s, hs, hμs⟩
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
hν : ν.FiniteAtFilter l'
s : Set X
hs : s ∈ l
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')
have rcases : ∀ (t : Set Y) (ht : t ∈ l') (hνt : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  (μ.prod ν).FiniteAtFilter (l ×ˢ l')
Tactic: rcases hν with ⟨t, ht, hνt⟩
Cleared hypotheses: hν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Y
ht : t ∈ l'
hνt : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')
have right : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: use s ×ˢ t, Filter.prod_mem_prod hs ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
X : Type u_4
Y : Type u_5
m : MeasurableSpace X
μ : Measure X
m' : MeasurableSpace Y
ν : Measure Y
l : Filter X
l' : Filter Y
s : Set X
hs : s ∈ l
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set Y
ht : t ∈ l'
hνt : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have right : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) < ∞
Tactic: grw [prod_prod_le]
-- 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 γ
μ_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 : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x)
have rw : (μ.prod ν).FiniteAtFilter (𝓝 x.1 ×ˢ 𝓝 x.2)
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
⊢ IsFiniteMeasure (μ.prod ν)
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
Tactic: rw [← univ_prod_univ, prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
rw :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
Tactic: rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
rw :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
Tactic: rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
rw :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₃ : HMul.hMul (α := ℝ≥0∞) 1 1 = 1
Tactic: rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_4 : IsProbabilityMeasure μ
inst_5 : IsProbabilityMeasure ν
rw :
  Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
rw₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 1
rw₃ : HMul.hMul (α := ℝ≥0∞) 1 1 = 1
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]
-- 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 γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : PseudoMetricSpace X
inst_5 : MeasurableSpace X
inst_6 : PseudoMetricSpace Y
inst_7 : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst_8 : SFinite ν
inst_9 : IsUnifLocDoublingMeasure μ
inst_10 : IsUnifLocDoublingMeasure ν
⊢ IsUnifLocDoublingMeasure (μ.prod ν)
have exists_measure_closedBall_le_mul'' : ∃ (C : NNReal),
  ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∀ (x : X × Y),
      (μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
Tactic: constructor
-- 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 γ
μ_1 μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
X : Type u_4
Y : Type u_5
inst_4 : PseudoMetricSpace X
inst_5 : MeasurableSpace X
inst_6 : PseudoMetricSpace Y
inst_7 : MeasurableSpace Y
μ : Measure X
ν : Measure Y
inst_8 : SFinite ν
inst_9 : IsUnifLocDoublingMeasure μ
inst_10 : IsUnifLocDoublingMeasure ν
⊢ ∃ (C : NNReal),
    ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
      ∀ (x : X × Y),
        (μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
have h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
  ∀ (x : X × Y),
    (μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x (2 * ε)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞)
        ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x ε) : ℝ≥0∞)
Tactic: use doublingConstant μ * doublingConstant ν