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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₃ :
  ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
    ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₃ :
  ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₄ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₅ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₁ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₂ : ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₃ : ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₃ :
  ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₄ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
    ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
simp_rw :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' toMeasurable μ s ×ˢ T) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₁ :
  ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (if x ∈ toMeasurable μ s then T else ∅) ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₂ :
  ∫⁻ (x : α), (toMeasurable μ s).indicator (fun (x : α) ↦ (ν : (a : Set β) → ℝ≥0∞) T) x ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₃ :
  ∫⁻ (x : α) in toMeasurable μ s, (ν : (a : Set β) → ℝ≥0∞) T ∂μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
simp_rw₄ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
      ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν : (a : Set β) → ℝ≥0∞) 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∞)
have simp_rw₅ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) T : ℝ≥0∞)
Tactic: classical
      simp_rw [S, mk_preimage_prod_right_eq_if, measure_if,
        lintegral_indicator (measurableSet_toMeasurable _ _), lintegral_const,
        restrict_apply_univ, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν 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∞)
have rw : 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: rw [measure_toMeasurable, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
rw :
  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∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : 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: rw [measure_toMeasurable, 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 β
s : Set α
t : Set β
S : Set α := toMeasurable μ s
T : Set β := toMeasurable ν t
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have ν₁ : LE.le (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
  ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (S ×ˢ 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]
-- 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 α
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∞)
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have ν₂ : ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' 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]
-- 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 α
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∞)
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
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
    μ.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]
-- 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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : NoAtoms μ
x : α
y : β
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) {x} {y}) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [singleton_prod_singleton]
-- 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 γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst_3 : NoAtoms ν
x : α
y : β
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) {x} {y}) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [singleton_prod_singleton]
-- 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
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s = ∫⁻ (x : α), (ν : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂μ
have simp_rw : (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (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]
-- 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
simp_rw :
  (μ.bind fun (x : α) ↦ map (Prod.mk x) ν : (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) ∂μ
have simp_rw₁ : ∫⁻ (a : α), (map (Prod.mk a) ν : (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]
-- 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 β
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
have apply : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
  (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
Tactic: apply (prod_prod_le s t).antisymm
-- 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 α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have hSTm : MeasurableSet ST
Tactic: have hSTm : MeasurableSet ST := measurableSet_toMeasurable _ _
-- 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 α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
hSTm : MeasurableSet ST
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have hST : s ×ˢ t ⊆ ST
Tactic: have hST : s ×ˢ t ⊆ ST := subset_toMeasurable _ _
-- 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 α
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)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have hfm : Measurable f
Tactic: have hfm : Measurable f := measurable_measure_prodMk_left hSTm
-- 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 α
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}
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t)
have hss' : s ⊆ s'
Tactic: have hss' : s ⊆ s' := fun x hx => measure_mono fun y hy => hST <| mk_mem_prod hx hy
-- 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∞) =
    ∫⁻ (x : α) in s', (ν : (a : Set β) → ℝ≥0∞) t ∂μ
have 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∞)
Tactic: rw [setLIntegral_const, mul_comm]