awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ν
⊢ ∀ᶠ (ε : ℝ) 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∞)
have 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∞)
Tactic: filter_upwards [eventually_measure_le_doublingConstant_mul μ,
    eventually_measure_le_doublingConstant_mul ν] with r hμr hνr x
-- 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 ν
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∞)
have 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∞)
Tactic: rw [← closedBall_prod_same, prod_prod, ← closedBall_prod_same, prod_prod]
-- 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 ν
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
⊢ 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∞)
have h : HMul.hMul (β := ℝ≥0∞)
    (HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 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∞)
Tactic: grw [hμr, hνr, ENNReal.coe_mul, mul_mul_mul_comm]
-- 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 ν
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∞)
      (HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 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∞)
⊢ 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∞)
have h₁ : HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞) *
    HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.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∞)
Tactic: grw [hμr, hνr, ENNReal.coe_mul, mul_mul_mul_comm]
-- 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 ν
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∞)
      (HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 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∞)
h₁ :
  HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.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∞)
⊢ 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∞)
have h₂ : HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant μ) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (Metric.closedBall x.1 r) : ℝ≥0∞) *
    HMul.hMul (β := ℝ≥0∞) (↑(doublingConstant ν) : ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) (Metric.closedBall x.2 r) : ℝ≥0∞) ≤
  (↑(doublingConstant μ) : ℝ≥0∞) * (↑(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∞)
Tactic: grw [hμr, hνr, ENNReal.coe_mul, mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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 : α) ∂μ, LT.lt (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h2s₁ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ ≠ ∞
Tactic: rw [prod_apply hs] at h2s
Cleared hypotheses: h2s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have ν₁ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ = 0
Tactic: calc
    μ.prod ν s ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hsm
    _ = 0 := by simp [lintegral_congr_ae 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 ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
have rw : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ = 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)]
-- 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 (α × β)
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
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
have 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
Tactic: rw [prod_apply hs, lintegral_eq_zero_iff (measurable_measure_prodMk_left 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 ν
s : Set (α × β)
h : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
have 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
Tactic: obtain ⟨t, hst, mt, ht⟩ := exists_measurable_superset_of_null h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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 ⁻¹' s)) 0
have ht₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' t)) 0
Tactic: rw [measure_prod_null mt] at ht
Cleared hypotheses: ht
-- 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 (α × β)
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 μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
have 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)
Tactic: rw [eventuallyLE_antisymm_iff]
-- 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 ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
⊢ μ.prod ν ≪ μ'.prod ν'
have 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∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs h2s => ?_
-- 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 ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
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∞)
have apply : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
Tactic: apply measure_prod_null_of_ae_null hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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
have h2s₁ : (ae μ').EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (ν' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s)) 0
Tactic: rw [measure_prod_null hs] at h2s
Cleared hypotheses: h2s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.fst (μ.prod ν) μ
have 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∞)
Tactic: refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map Prod.fst (μ.prod ν) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (β := Set β) s univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply measurable_fst hs, ← prod_univ, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
have refine : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
Tactic: refine (prod_prod_le _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
Tactic: rw [h2s, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [h2s, zero_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
⊢ QuasiMeasurePreserving Prod.snd (μ.prod ν) ν
have 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∞)
Tactic: refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((map Prod.snd (μ.prod ν) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [map_apply measurable_snd hs, ← univ_prod, ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
have refine : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = 0
Tactic: refine (prod_prod_le _ _).trans_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = 0
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) = 0
Tactic: rw [h2s, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [h2s, mul_zero]
-- 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 β
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∞) (s ×ˢ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: rw [Set.compl_prod_eq_union, measure_union_null_iff]
-- 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 β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet t ν
have rcases : ∀ (u : Set (α × β)) (hum : MeasurableSet u) (hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u), NullMeasurableSet t ν
Tactic: rcases h with ⟨u, hum, hu⟩
Cleared hypotheses: h