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 κ
μ_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))
⊢ 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:
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))
-- 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
⊢ ∀ {μ : 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))
-- 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
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)) : ℝ)) ∂μ
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)) : ℝ)) ∂ν)
⊢ (∫⁻ (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

Tactic:
simp_rw [this]
-- 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
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)) : ℝ)) ∂μ
i : ι
⊢ Continuous[inst i, _] fun (x : X i) ↦ (↑((f i : (a : X i) → ℝ≥0) 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 κ
μ ν : 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)) : ℝ)) ∂μ
j : κ
⊢ Continuous[inst_3 j, _] fun (y : Y j) ↦ (↑((g j : (a : Y j) → ℝ≥0) y) : ℝ)

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 κ
μ ν : 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)) : ℝ)) ∂μ
⊢ 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:
exact h (fun i ↦ ⟨⟨fun x ↦ (f i x), by fun_prop⟩, (f i).map_bounded'⟩)
      (fun j ↦ ⟨⟨fun y ↦ (g j y), by fun_prop⟩, (g j).map_bounded'⟩)

Premises used: ContinuousMap.mk, BoundedContinuousFunction.mk, BoundedContinuousFunction.map_bounded', DFunLike.coe, NNReal.toReal
-- 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
i : ι
⊢ Continuous[instTopologicalSpaceProd, inst i] (Function.eval (β := X) i ∘ Prod.fst)

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 κ
μ ν : 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
j : κ
⊢ Continuous[instTopologicalSpaceProd, inst_3 j] (Function.eval (β := Y) j ∘ Prod.snd)

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 κ
μ ν : 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
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 := ⋯ :
                      C(((x : ι) → X x) × ((x : κ) → Y x), X i) })
                (∏ j : κ,
                  (g j).compContinuous
                    { toFun := Function.eval (β := Y) j ∘ Prod.snd, continuous_toFun := ⋯ :
                      C(((x : ι) → X x) × ((x : κ) → Y x), Y j) }) :
              (a : ((i : ι) → X i) × ((j : κ) → Y j)) → ℝ≥0)
            x) :
        ℝ≥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:
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

Premises used: HMul.hMul, Finset.univ, ContinuousMap.mk, BoundedContinuousFunction.lintegral_lt_top_of_nnreal, Function.comp, Function.eval, BoundedContinuousFunction.compContinuous, Prod.fst, Finset.prod, Prod.snd, LT.lt.ne
-- 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
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 := ⋯ :
                    C(((x : ι) → X x) × ((x : κ) → Y x), X i) })
              (∏ j : κ,
                (g j).compContinuous
                  { toFun := Function.eval (β := Y) j ∘ Prod.snd, continuous_toFun := ⋯ :
                    C(((x : ι) → X x) × ((x : κ) → Y x), Y j) }) :
            (a : ((i : ι) → X i) × ((j : κ) → Y j)) → ℝ≥0)
          x) :
      ℝ≥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 μ
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
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 := ⋯ :
                      C(((x : ι) → X x) × ((x : κ) → Y x), X i) })
                (∏ j : κ,
                  (g j).compContinuous
                    { toFun := Function.eval (β := Y) j ∘ Prod.snd, continuous_toFun := ⋯ :
                      C(((x : ι) → X x) × ((x : κ) → Y x), Y j) }) :
              (a : ((i : ι) → X i) × ((j : κ) → Y j)) → ℝ≥0)
            x) :
        ℝ≥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:
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

Premises used: HMul.hMul, Finset.univ, ContinuousMap.mk, BoundedContinuousFunction.lintegral_lt_top_of_nnreal, Function.comp, Function.eval, BoundedContinuousFunction.compContinuous, Prod.fst, Finset.prod, Prod.snd, LT.lt.ne
-- 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)
ν : 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 ν
rw₁ 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 ν)
⊢ 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 ν)

Tactic:
rw [h, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
T : Type u_4
X : ι → Type u_5
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)
mT : MeasurableSpace T
inst_3 : TopologicalSpace T
inst_4 : BorelSpace T
inst_5 : HasOuterApproxClosed T
inst_6 : Fintype ι
μ ν : Measure (((i : ι) → X i) × T)
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : T →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ν)
p : ((i : ι) → X i) × T
⊢ (fun (p : ((i : ι) → X i) × (Unit → T)) ↦ ((fun (i : ι) ↦ p.1 i, p.2 ()) : ((i : ι) → X i) × T))
      ((fun (p : ((i : ι) → X i) × T) ↦ ((fun (i : ι) ↦ p.1 i, fun (x : Unit) ↦ p.2) : ((i : ι) → X i) × (Unit → T)))
        p) =
    p

Tactic:
simp