awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 μ
h :
  ∀ (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∞) ∂μ =
      ∫⁻ (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∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
hp1 :
  ∀ (x : (i : ι) → X i),
    Eq (α := ℝ≥0) (∏ i : ι, (s i).indicator (fun (x : X i) ↦ 1) (x i)) ((Set.pi (α := X) univ s).indicator 1 x)
hp2 :
  ∀ (y : (j : κ) → Y j),
    Eq (α := ℝ≥0) (∏ j : κ, (t j).indicator (fun (x : Y j) ↦ 1) (y j)) ((Set.pi (α := Y) univ t).indicator 1 y)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop (𝓝 (↑((Set.pi (α := X) univ s ×ˢ Set.pi (α := Y) univ t).indicator 1 p) : ℝ≥0∞))
h1 :
  Tendsto
    (fun (n : ℕ) ↦
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(HMul.hMul (α := ℝ≥0) (∏ i : ι, (⋯.apprSeq (F := s i) n : (a : X i) → ℝ≥0) (p.1 i))
              (∏ j : κ, (⋯.apprSeq (F := t j) n : (a : Y j) → ℝ≥0) (p.2 j))) :
          ℝ≥0∞) ∂μ)
    atTop
    (𝓝
      (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑((Set.pi (α := X) univ s ×ˢ Set.pi (α := Y) univ t).indicator 1 p) : ℝ≥0∞) ∂μ))
x : ℕ
x_1 : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ ∀ (i : κ),
    Membership.mem (γ := Finset κ) Finset.univ i →
      LE.le (α := ℝ≥0) (0 : ℝ≥0) ((⋯.apprSeq (F := t i) x : (a : Y i) → ℝ≥0) (x_1.2 i) : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 μ
h :
  ∀ (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∞) ∂μ =
      ∫⁻ (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∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this_1 : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst i] (s i)
ht : ∀ (i : κ), IsClosed[inst_3 i] (t i)
hp1 :
  ∀ (x : (i : ι) → X i),
    Eq (α := ℝ≥0) (∏ i : ι, (s i).indicator (fun (x : X i) ↦ 1) (x i)) ((Set.pi (α := X) univ s).indicator 1 x)
hp2 :
  ∀ (y : (j : κ) → Y j),
    Eq (α := ℝ≥0) (∏ j : κ, (t j).indicator (fun (x : Y j) ↦ 1) (y j)) ((Set.pi (α := Y) univ t).indicator 1 y)
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (α := ℕ)
      (ofNNReal ∘ fun (x : ℕ) ↦
        HMul.hMul (α := ℝ≥0) (∏ c : ι, (⋯.apprSeq (F := s c) x : (a : X c) → ℝ≥0) (p.1 c))
          (∏ c : κ, (⋯.apprSeq (F := t c) x : (a : Y c) → ℝ≥0) (p.2 c)))
      atTop (𝓝 (↑((Set.pi (α := X) univ s ×ˢ Set.pi (α := Y) univ t).indicator 1 p) : ℝ≥0∞))
h1 :
  Tendsto
    (fun (n : ℕ) ↦
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(HMul.hMul (α := ℝ≥0) (∏ i : ι, (⋯.apprSeq (F := s i) n : (a : X i) → ℝ≥0) (p.1 i))
              (∏ j : κ, (⋯.apprSeq (F := t j) n : (a : Y j) → ℝ≥0) (p.2 j))) :
          ℝ≥0∞) ∂μ)
    atTop
    (𝓝
      (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑((Set.pi (α := X) univ s ×ˢ Set.pi (α := Y) univ t).indicator 1 p) : ℝ≥0∞) ∂μ))
x : ℕ
x_1 : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ (↑1 : ℝ≥0∞) * (↑1 : ℝ≥0∞) ≤ 1 x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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)) ∂ν)
⊢ μ = ν

Tactic:
ext_of_lintegral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_lintegral_prod_mul_prod_boundedContinuousFunction
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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)) ∂ν)
refine :
  ∀ (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∞) ∂μ =
      ∫⁻ (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∞) ∂ν
⊢ μ = ν

Tactic:
refine ext_of_lintegral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_lintegral_prod_mul_prod_boundedContinuousFunction
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
rw :
  (∫⁻ (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∞) ∂μ).toReal =
    (∫⁻ (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∞) ∂ν).toReal
hx :
  ∫⁻ (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∞) ∂μ ≠
    ∞
hy :
  ∫⁻ (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∞) ∂ν ≠
    ∞
⊢ ∫⁻ (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∞) ∂μ =
    ∫⁻ (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∞) ∂ν

Tactic:
rw [← toReal_eq_toReal_iff']

Premises used: ENNReal.toReal_eq_toReal_iff'
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
simp :
  (∫⁻ (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
⊢ (∫⁻ (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∞) ∂μ).toReal =
    (∫⁻ (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∞) ∂ν).toReal

Tactic:
simp only [coe_finsetProd]

Premises used: ENNReal.coe_finsetProd
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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)) : ℝ))
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)) : ℝ)))
    μ
⊢ (∫⁻ (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:
rw [integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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))
⊢ (∫⁻ (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

Tactic:
simp [Finset.prod_nonneg, ofReal_prod_of_nonneg]

Premises used: ENNReal.ofReal_prod_of_nonneg, Finset.prod_nonneg
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ LE.le (α := ℝ) (0 x)
    ((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)) : ℝ)))
      x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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))
⊢ (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:
exact Eventually.of_forall fun _ ↦ by positivity

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
funProp₁ : MeasurableEmbedding (β := ℝ≥0) fun (p1 : X x) ↦ (f x : (a : X x) → ℝ≥0) p1
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (f x : (a : X x) → ℝ≥0) (p.1 x)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
funProp₁ : MeasurableEmbedding (β := ℝ≥0) fun (p1 : Y x) ↦ (g x : (a : Y x) → ℝ≥0) p1
⊢ Measurable (β := ℝ≥0) fun (p : ((i : ι) → X i) × ((j : κ) → Y j)) ↦ (g x : (a : Y x) → ℝ≥0) (p.2 x)

Tactic:
fun_prop