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 γ
μ_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 Y) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
v_open.measure_pos ν ⟨y, yv⟩

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 Y) → ℝ≥0∞) v : ℝ≥0∞)

Tactic:
exact v_open.measure_pos ν ⟨y, yv⟩

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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : MeasureSpace X
inst_6 : IsOpenPosMeasure.{u_4} (X := X) (m := MeasureSpace.toMeasurableSpace) volume
inst_7 : TopologicalSpace Y
inst_8 : MeasureSpace Y
inst_9 : IsOpenPosMeasure.{u_5} (X := Y) (m := MeasureSpace.toMeasurableSpace) volume
inst_10 : SFinite.{u_5} (α := Y) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsOpenPosMeasure (X := X × Y) (m := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instIsOpenPosMeasure

Premises used: MeasureTheory.Measure.prod.instIsOpenPosMeasure
-- Module: Mathlib.MeasureTheory.Measure.Prod
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'
rcases :
  ∀ (s : Set X) (hs : s ∈ l) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (μ.prod ν).FiniteAtFilter (l ×ˢ l')
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')

Tactic:
rcases hμ with ⟨s, hs, hμs⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
rcases :
  ∀ (t : Set Y) (ht : t ∈ l') (hνt : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    (μ.prod ν).FiniteAtFilter (l ×ˢ l')
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')

Tactic:
rcases hν with ⟨t, ht, hνt⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
right : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ.prod ν).FiniteAtFilter (l ×ˢ l')

Tactic:
use s ×ˢ t, Filter.prod_mem_prod hs ht

Premises used: Filter.prod_mem_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
right : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
grw [prod_prod_le]

Premises used: MeasureTheory.Measure.prod_prod_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top hμs hνt

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.mul_lt_top hμs hνt

Premises used: ENNReal.mul_lt_top
-- 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 : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : IsLocallyFiniteMeasure ν
x : X × Y
rw : (μ.prod ν).FiniteAtFilter (𝓝 x.1 ×ˢ 𝓝 x.2)
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x)

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- 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 : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x.1 ×ˢ 𝓝 x.2)

Tactic:
μ.finiteAt_nhds _ |>.prod <| ν.finiteAt_nhds _

Premises used: MeasureTheory.Measure.finiteAt_nhds, MeasureTheory.Measure.FiniteAtFilter.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 : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst_7 : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x.1 ×ˢ 𝓝 x.2)

Tactic:
exact μ.finiteAt_nhds _ |>.prod <| ν.finiteAt_nhds _

Premises used: MeasureTheory.Measure.finiteAt_nhds, MeasureTheory.Measure.FiniteAtFilter.prod
-- 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 : SFinite ν
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : TopologicalSpace Y
m : MeasureSpace X
inst_6 : IsLocallyFiniteMeasure.{u_4} (α := X) (m0 := MeasureSpace.toMeasurableSpace) volume
m' : MeasureSpace Y
inst_7 : IsLocallyFiniteMeasure.{u_5} (α := Y) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsLocallyFiniteMeasure (α := X × Y) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instIsLocallyFiniteMeasure

Premises used: MeasureTheory.Measure.prod.instIsLocallyFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure (μ.prod ν)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
measure_univ_lt_top :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← univ_prod_univ, prod_prod]

Premises used: MeasureTheory.Measure.prod_prod, Set.univ_prod_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ μ' : Measure α_1
ν ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν
α : Type u_4
β : Type u_5
inst_4 : MeasureSpace α
inst_5 : MeasureSpace β
inst_6 : IsFiniteMeasure.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : IsFiniteMeasure.{u_5} (α := β) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsFiniteMeasure (α := α × β) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instIsFiniteMeasure _ _

Premises used: MeasureTheory.Measure.prod.instIsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw₄ rw₅ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.Measure.prod_prod, Set.univ_prod_univ, mul_one
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ μ' : Measure α_1
ν ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν
α : Type u_4
β : Type u_5
inst_4 : MeasureSpace α
inst_5 : MeasureSpace β
inst_6 : IsProbabilityMeasure.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : IsProbabilityMeasure.{u_5} (α := β) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsProbabilityMeasure (α := α × β) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instIsProbabilityMeasure _ _

Premises used: MeasureTheory.Measure.prod.instIsProbabilityMeasure
-- 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 : SFinite ν
X : Type u_4
Y : Type u_5
inst_4 : TopologicalSpace X
inst_5 : MeasureSpace X
inst_6 : IsFiniteMeasureOnCompacts.{u_4} (α := X) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_7 : TopologicalSpace Y
inst_8 : MeasureSpace Y
inst_9 : IsFiniteMeasureOnCompacts.{u_5} (α := Y) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ IsFiniteMeasureOnCompacts (α := X × Y) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instIsFiniteMeasureOnCompacts _ _

Premises used: MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts
-- 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 : 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 ν
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∞)
⊢ IsUnifLocDoublingMeasure (μ.prod ν)

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 : 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 ν
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∞)
⊢ ∃ (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:
use doublingConstant μ * doublingConstant ν

Premises used: IsUnifLocDoublingMeasure.doublingConstant
-- 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 : 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 ν
h :
  ∀ (r : ℝ)
    (hμr :
      ∀ (x : X),
        (μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞)
            ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞))
    (hνr :
      ∀ (x : Y),
        (ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞)
            ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞))
    (x : X × Y),
    (μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞)
        ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
⊢ ∀ᶠ (ε : ℝ) 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:
filter_upwards [eventually_measure_le_doublingConstant_mul μ,
    eventually_measure_le_doublingConstant_mul ν] with r hμr hνr x

Premises used: IsUnifLocDoublingMeasure.eventually_measure_le_doublingConstant_mul
-- 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 : 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 ν
r : ℝ
hμr :
  ∀ (x : X),
    (μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
hνr :
  ∀ (x : Y),
    (ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)
x : X × Y
h :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 (2 * r)) : ℝ≥0∞)
      ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 (2 * r)) : ℝ≥0∞) ≤
    (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞)
        ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞)
⊢ (μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x (2 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ * doublingConstant ν) : ℝ≥0∞)
      ((μ.prod ν : (a : Set (X × Y)) → ℝ≥0∞) (Metric.closedBall x r) : ℝ≥0∞)

Tactic:
rw [← closedBall_prod_same, prod_prod, ← closedBall_prod_same, prod_prod]

Premises used: MeasureTheory.Measure.prod_prod, closedBall_prod_same
-- 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 : SFinite ν
X : Type u_4
Y : Type u_5
inst_4 : PseudoMetricSpace X
inst_5 : MeasureSpace X
inst_6 : PseudoMetricSpace Y
inst_7 : MeasureSpace Y
inst_8 : SFinite.{u_5} (α := Y) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_9 : IsUnifLocDoublingMeasure.{u_4} (α := X) volume
inst_10 : IsUnifLocDoublingMeasure.{u_5} (α := Y) volume
⊢ IsUnifLocDoublingMeasure (α := X × Y) volume

Tactic:
.prod _ _

Premises used: IsUnifLocDoublingMeasure.prod
-- 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
h2s : Ne (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ ≠ ∞

Tactic:
rw [prod_apply hs] at h2s

Premises used: MeasureTheory.Measure.prod_apply
-- 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
h2s : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
ae_lt_top (measurable_measure_prodMk_left hs) h2s

Premises used: measurable_measure_prodMk_left, MeasureTheory.ae_lt_top
-- 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
h2s : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ae_lt_top (measurable_measure_prodMk_left hs) h2s

Premises used: measurable_measure_prodMk_left, MeasureTheory.ae_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: 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 (α × β)
hsm : MeasurableSet s
hs : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s ≤ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ

Tactic:
prod_apply_le hsm

Premises used: MeasureTheory.Measure.prod_apply_le
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
⊢ ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ = 0

Tactic:
simp [lintegral_congr_ae hs]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set (α × β)
hsm : MeasurableSet s
hs : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
ν₁ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ = 0
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
calc
    μ.prod ν s ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hsm
    _ = 0 := by simp [lintegral_congr_ae hs]

Premises used: MeasureTheory.Measure.prod_apply_le, MeasureTheory.Measure.prod, 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 (α × β)
hs : MeasurableSet s
rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ = 0 ↔
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
rw₁ rw₂ :
  (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
⊢ 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 [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prodMk_left hs)]

Premises used: MeasureTheory.lintegral_eq_zero_iff, MeasureTheory.Measure.prod_apply, measurable_measure_prodMk_left