awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
rw :
  (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
    (∫⁻ (a : ((i : ι) → X i) × ((j : κ) → Y j)),
        ENNReal.ofReal
          (HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (a.1 i)) : ℝ))
            (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (a.2 j)) : ℝ))) ∂μ).toReal
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
        (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂μ
have hf : (ae μ).EventuallyLE (β := ℝ) 0 fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦
  HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
    (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ))
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
rw :
  (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
    (∫⁻ (a : ((i : ι) → X i) × ((j : κ) → Y j)),
        ENNReal.ofReal
          (HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (a.1 i)) : ℝ))
            (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (a.2 j)) : ℝ))) ∂μ).toReal
hf :
  (ae μ).EventuallyLE (β := ℝ) 0 fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦
    HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
      (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ))
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
        (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂μ
have hfm : AEStronglyMeasurable (β := ℝ)
  (fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦
    HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
      (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)))
  μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
x : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ x
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (f x : (a : X x) → ℝ≥0) (p.1 x)
have funProp : mX x ≤ mX x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
x : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ x
funProp : mX x ≤ mX x
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (f x : (a : X x) → ℝ≥0) (p.1 x)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0) fun (p1 : X x) ↦ (f x : (a : X x) → ℝ≥0) p1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
x : κ
h_1 : Membership.mem (γ := Finset κ) Finset.univ x
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (g x : (a : Y x) → ℝ≥0) (p.2 x)
have funProp : mY x ≤ mY x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ_1 ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ_1
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ_1)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
x : κ
h_1 : Membership.mem (γ := Finset κ) Finset.univ x
funProp : mY x ≤ mY x
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (g x : (a : Y x) → ℝ≥0) (p.2 x)
have funProp₁ : MeasurableEmbedding (β := ℝ≥0) fun (p1 : Y x) ↦ (g x : (a : Y x) → ℝ≥0) p1
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ a : ι, (↑((f a : (a : X a) → ℝ≥0) (p.1 a)) : ℝ≥0∞))
          (∏ a : κ, (↑((g a : (a : Y a) → ℝ≥0) (p.2 a)) : ℝ≥0∞)) ∂μ).toReal =
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ a : ι, (↑((f a : (a : X a) → ℝ≥0) (p.1 a)) : ℝ≥0∞))
          (∏ a : κ, (↑((g a : (a : Y a) → ℝ≥0) (p.2 a)) : ℝ≥0∞)) ∂ν).toReal
have this : ∀ {μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))},
  (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
        (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂μ
Tactic: have {μ : Measure ((Π i, X i) × Π j, Y j)} :
        (∫⁻ p, (∏ i, (f i (p.1 i) : ℝ≥0∞)) * ∏ j, (g j (p.2 j) : ℝ≥0∞) ∂μ).toReal =
          ∫ p, (∏ i, (f i (p.1 i)).toReal) * ∏ j, (g j (p.2 j)).toReal ∂μ := by
      rw [integral_eq_lintegral_of_nonneg_ae]
      · simp [Finset.prod_nonneg, ofReal_prod_of_nonneg]
      · exact Eventually.of_forall fun _ ↦ by positivity
      exact AEStronglyMeasurable.mul
        (Finset.aestronglyMeasurable_fun_prod _ fun _ _ ↦
          continuous_coe.aestronglyMeasurable.comp_measurable (by fun_prop))
        (Finset.aestronglyMeasurable_fun_prod _ fun _ _ ↦
          continuous_coe.aestronglyMeasurable.comp_measurable (by fun_prop))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
this :
  ∀ {μ : Measure (((i : ι) → X i) × ((j : κ) → Y j))},
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
          HMul.hMul (α := ℝ≥0∞) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞))
            (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞)) ∂μ).toReal =
      ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
          (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂μ
⊢ (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ a : ι, (↑((f a : (a : X a) → ℝ≥0) (p.1 a)) : ℝ≥0∞))
          (∏ a : κ, (↑((g a : (a : Y a) → ℝ≥0) (p.2 a)) : ℝ≥0∞)) ∂μ).toReal =
    (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ≥0∞) (∏ a : ι, (↑((f a : (a : X a) → ℝ≥0) (p.1 a)) : ℝ≥0∞))
          (∏ a : κ, (↑((g a : (a : Y a) → ℝ≥0) (p.2 a)) : ℝ≥0∞)) ∂ν).toReal
have simp_rw : Eq (α := ℝ)
  (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
      (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂μ)
  (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (∏ i : ι, (↑((f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ))
      (∏ j : κ, (↑((g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ)) ∂ν)
Tactic: simp_rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
⊢ ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ ≠
    ∞
have h₁ : ∀ (x : ((i : ι) → X i) × ((j : κ) → Y j)),
  (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (x.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (x.2 j)) : ℝ≥0∞) =
    (↑((HMul.hMul (α := ((x : ι) → X x) × ((x : κ) → Y x) →ᵇ ℝ≥0)
              (∏ i : ι,
                (f i).compContinuous
                  { toFun := Function.eval (β := X) i ∘ Prod.fst, continuous_toFun := sorry :
                    C(((x : ι) → X x) × ((x : κ) → Y x), X i) })
              (∏ j : κ,
                (g j).compContinuous
                  { toFun := Function.eval (β := Y) j ∘ Prod.snd, continuous_toFun := sorry :
                    C(((x : ι) → X x) × ((x : κ) → Y x), Y j) }) :
            (a : ((i : ι) → X i) × ((j : κ) → Y j)) → ℝ≥0)
          x) :
      ℝ≥0∞)
Tactic: convert!
    (lintegral_lt_top_of_nnreal μ
        ((∏ i, (f i).compContinuous ⟨Function.eval i ∘ Prod.fst, by fun_prop⟩) *
          (∏ j, (g j).compContinuous ⟨Function.eval j ∘ Prod.snd, by fun_prop⟩))).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ν)
f : (i : ι) → X i →ᵇ ℝ≥0
g : (j : κ) → Y j →ᵇ ℝ≥0
⊢ ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν ≠
    ∞
have h₁ : ∀ (x : ((i : ι) → X i) × ((j : κ) → Y j)),
  (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (x.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (x.2 j)) : ℝ≥0∞) =
    (↑((HMul.hMul (α := ((x : ι) → X x) × ((x : κ) → Y x) →ᵇ ℝ≥0)
              (∏ i : ι,
                (f i).compContinuous
                  { toFun := Function.eval (β := X) i ∘ Prod.fst, continuous_toFun := sorry :
                    C(((x : ι) → X x) × ((x : κ) → Y x), X i) })
              (∏ j : κ,
                (g j).compContinuous
                  { toFun := Function.eval (β := Y) j ∘ Prod.snd, continuous_toFun := sorry :
                    C(((x : ι) → X x) × ((x : κ) → Y x), Y j) }) :
            (a : ((i : ι) → X i) × ((j : κ) → Y j)) → ℝ≥0)
          x) :
      ℝ≥0∞)
Tactic: convert!
    (lintegral_lt_top_of_nnreal ν
        ((∏ i, (f i).compContinuous ⟨Function.eval i ∘ Prod.fst, by fun_prop⟩) *
          (∏ j, (g j).compContinuous ⟨Function.eval j ∘ Prod.snd, by fun_prop⟩))).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ : Measure ((i : ι) → X i)
ν : Measure ((j : κ) → Y j)
ξ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
inst_10 : IsFiniteMeasure ξ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
        (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν)
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ξ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
    (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν) =
  ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ.prod ν
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : Fintype ι
inst_7 : Fintype κ
μ : Measure ((i : ι) → X i)
ν : Measure ((j : κ) → Y j)
ξ : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
inst_9 : IsFiniteMeasure ν
inst_10 : IsFiniteMeasure ξ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
        (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν)
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
      (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν) =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ.prod ν
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂ξ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (z.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (z.2 j)) ∂μ.prod ν)
  (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j)) ∂μ.prod ν)
Tactic: rw [h, ← integral_prod_mul]