awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst : TopologicalSpace Z
inst_1 : BorelSpace Z
inst_2 : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst_3 : TopologicalSpace T
inst_4 : BorelSpace T
inst_5 : HasOuterApproxClosed T
μ : Measure Z
ν : Measure T
ξ : Measure (Z × T)
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
inst_8 : IsFiniteMeasure ξ
h :
  ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
f : Z →ᵇ ℝ
g : T →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
  ∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
Z : Type u_3
T : Type u_4
mZ : MeasurableSpace Z
inst : TopologicalSpace Z
inst_1 : BorelSpace Z
inst_2 : HasOuterApproxClosed Z
mT : MeasurableSpace T
inst_3 : TopologicalSpace T
inst_4 : BorelSpace T
inst_5 : HasOuterApproxClosed T
μ : Measure Z
ν : Measure T
ξ : Measure (Z × T)
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
inst_8 : IsFiniteMeasure ξ
h :
  ∀ (f : Z →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
f : Z →ᵇ ℝ
g : T →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
    ∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν
⊢ Eq (α := ℝ) (∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) z.1 : ℝ) ((g : (a : T) → ℝ) z.2 : ℝ) ∂μ.prod ν)
  (∫ (p : Z × T), HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.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 : Finite ι
inst_7 : Finite κ
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
⊢ μ = ν
have have : ∀ (this : Fintype ι), μ = ν
Tactic: have := Fintype.ofFinite ι
-- 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 : Finite ι
inst_7 : Finite κ
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
this : Fintype ι
⊢ μ = ν
have have : ∀ (this : Fintype κ), μ = ν
Tactic: have := Fintype.ofFinite κ
-- 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 : Finite ι
inst_7 : Finite κ
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
this_1 : Fintype ι
this : Fintype κ
⊢ μ = ν
have refine : ∀ (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: refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
-- 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 : Finite ι
inst_7 : Finite κ
μ : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ)
        (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν)
f : ((i : ι) → X i) →ᵇ ℝ
g : ((j : κ) → Y j) →ᵇ ℝ
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ)
        ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ)
    (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν) =
  ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ)
      ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.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 : Finite ι
inst_7 : Finite κ
μ : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ)
        (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν)
f : ((i : ι) → X i) →ᵇ ℝ
g : ((j : κ) → Y j) →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ)
      (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν) =
    ∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ)
        ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ)
        ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) z.1 : ℝ)
      ((g : (a : (j : κ) → Y j) → ℝ) z.2 : ℝ) ∂μ.prod ν)
  (∫ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ)
      ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
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 : Finite ι
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ν)
⊢ μ = ν
have have : ∀ (this : Fintype ι), μ = ν
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
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 : Finite ι
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ν)
this : Fintype ι
⊢ μ = ν
have refine : ∀ (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 : ℝ) ∂ν)
Tactic: refine ext_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
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 : Finite ι
μ ν : 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 (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ν)
this : Fintype ι
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 : ℝ) ∂ν)
have h₁ : ∀ (x : ((i : ι) → X i) × T),
  Eq (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (x.1 i) : ℝ)
    ((∏ i : ι, (f i).compContinuous { toFun := Function.eval (β := X) i, continuous_toFun := sorry } :
          (a : (i : ι) → X i) → ℝ)
        x.1 :
      ℝ)
Tactic: convert! h (∏ i, (f i).compContinuous ⟨Function.eval i, by fun_prop⟩) g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
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 : Finite ι
μ : Measure ((i : ι) → X i)
ν : Measure T
ξ : Measure (((i : ι) → X i) × T)
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
inst_9 : IsFiniteMeasure ξ
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
f : ((i : ι) → X i) →ᵇ ℝ
g : T →ᵇ ℝ
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
  ∫ (p : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
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 : Finite ι
μ : Measure ((i : ι) → X i)
ν : Measure T
ξ : Measure (((i : ι) → X i) × T)
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
inst_9 : IsFiniteMeasure ξ
h :
  ∀ (f : ((i : ι) → X i) →ᵇ ℝ) (g : T →ᵇ ℝ),
    ∫ (p : ((i : ι) → X i) × T),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
f : ((i : ι) → X i) →ᵇ ℝ
g : T →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), (f : (a : (i : ι) → X i) → ℝ) x ∂μ) (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
    ∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν
⊢ Eq (α := ℝ)
    (∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) z.1 : ℝ) ((g : (a : T) → ℝ) z.2 : ℝ) ∂μ.prod ν)
  (∫ (p : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : (i : ι) → X i) → ℝ) p.1 : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν)
Tactic: rw [h, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst : (j : κ) → TopologicalSpace (Y j)
inst_1 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_2 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
mZ : MeasurableSpace Z
inst_3 : TopologicalSpace Z
inst_4 : BorelSpace Z
inst_5 : HasOuterApproxClosed Z
inst_6 : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
⊢ μ = ν
have have : ∀ (this : Fintype κ), μ = ν
Tactic: have := Fintype.ofFinite κ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst : (j : κ) → TopologicalSpace (Y j)
inst_1 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_2 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
mZ : MeasurableSpace Z
inst_3 : TopologicalSpace Z
inst_4 : BorelSpace Z
inst_5 : HasOuterApproxClosed Z
inst_6 : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
this : Fintype κ
⊢ μ = ν
have refine : ∀ (f : Z →ᵇ ℝ) (g : (j : κ) → Y j →ᵇ ℝ),
  Eq (α := ℝ)
    (∫ (p : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂μ)
    (∫ (p : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂ν)
Tactic: refine ext_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst : (j : κ) → TopologicalSpace (Y j)
inst_1 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_2 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
mZ : MeasurableSpace Z
inst_3 : TopologicalSpace Z
inst_4 : BorelSpace Z
inst_5 : HasOuterApproxClosed Z
inst_6 : Finite κ
μ ν : Measure (Z × ((i : κ) → Y i))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    Eq (α := ℝ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ)
      (∫ (p : Z × ((i : κ) → Y i)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ν)
this : Fintype κ
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
⊢ Eq (α := ℝ)
    (∫ (p : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂μ)
    (∫ (p : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂ν)
have h₁ : ∀ (x : Z × ((j : κ) → Y j)),
  Eq (α := ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (x.2 j) : ℝ)
    ((∏ j : κ, (g j).compContinuous { toFun := Function.eval (β := Y) j, continuous_toFun := sorry } :
          (a : (j : κ) → Y j) → ℝ)
        x.2 :
      ℝ)
Tactic: convert! h f (∏ j, (g j).compContinuous ⟨Function.eval j, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd (goal)
Goal:
κ : Type u_2
Z : Type u_3
Y : κ → Type u_6
mY : (j : κ) → MeasurableSpace (Y j)
inst : (j : κ) → TopologicalSpace (Y j)
inst_1 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_2 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
mZ : MeasurableSpace Z
inst_3 : TopologicalSpace Z
inst_4 : BorelSpace Z
inst_5 : HasOuterApproxClosed Z
inst_6 : Finite κ
μ : Measure Z
ν : Measure ((j : κ) → Y j)
ξ : Measure (Z × ((j : κ) → Y j))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
inst_9 : IsFiniteMeasure ξ
h :
  ∀ (f : Z →ᵇ ℝ) (g : ((j : κ) → Y j) →ᵇ ℝ),
    ∫ (p : Z × ((j : κ) → Y j)),
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν)
f : Z →ᵇ ℝ
g : ((j : κ) → Y j) →ᵇ ℝ
⊢ Eq (α := ℝ)
    (∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂ξ)
    (∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ) (∫ (y : (j : κ) → Y j), (g : (a : (j : κ) → Y j) → ℝ) y ∂ν) =
  ∫ (p : Z × ((i : κ) → Y i)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν
Tactic: rw [h, ← integral_prod_mul]