awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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 : ℝ) ∂ν)
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun (p : ((i : ι) → X i) × T) ↦ (fun (i : ι) ↦ p.1 i, fun (x : Unit) ↦ p.2),
    invFun := fun (p : ((i : ι) → X i) × (Unit → T)) ↦ (fun (i : ι) ↦ p.1 i, p.2 ()), left_inv := ⋯, right_inv := ⋯,
    measurable_toFun := ⋯, measurable_invFun := ⋯ }
⊢ μ = ν
have rw : Eq (α := Measure (((i : ι) → X i) × (Unit → T)))
  (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) μ)
  (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) ν)
Tactic: rw [← e.map_measurableEquiv_injective.eq_iff]
-- 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 : 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 : ℝ) ∂ν)
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun (p : ((i : ι) → X i) × T) ↦ (fun (i : ι) ↦ p.1 i, fun (x : Unit) ↦ p.2),
    invFun := fun (p : ((i : ι) → X i) × (Unit → T)) ↦ (fun (i : ι) ↦ p.1 i, p.2 ()), left_inv := ⋯, right_inv := ⋯,
    measurable_toFun := ⋯, measurable_invFun := ⋯ }
⊢ Eq (α := Measure (((i : ι) → X i) × (Unit → T)))
    (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) μ)
    (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) ν)
have refine : ∀ (f : (i : ι) → X i →ᵇ ℝ) (g : (j : Unit) → T →ᵇ ℝ),
  Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) μ)
      fun (p : ((i : ι) → X i) × ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) ν)
      fun (p : ((i : ι) → X i) × ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (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
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 : ℝ) ∂ν)
e : ((i : ι) → X i) × T ≃ᵐ ((i : ι) → X i) × (Unit → T) :=
  { toFun := fun (p : ((i : ι) → X i) × T) ↦ (fun (i : ι) ↦ p.1 i, fun (x : Unit) ↦ p.2),
    invFun := fun (p : ((i : ι) → X i) × (Unit → T)) ↦ (fun (i : ι) ↦ p.1 i, p.2 ()), left_inv := ⋯, right_inv := ⋯,
    measurable_toFun := ⋯, measurable_invFun := ⋯ }
f : (i : ι) → X i →ᵇ ℝ
g : (j : Unit) → T →ᵇ ℝ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) μ)
      fun (p : ((i : ι) → X i) × ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.map (⇑e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × (Unit → T)) ν)
      fun (p : ((i : ι) → X i) × ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
have rw : Eq (α := ℝ)
  (∫ (x : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ)
      (∏ i : ι, (f i : (a : X i) → ℝ) (((e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × ((j : Unit) → T)) x).1 i))
      (∏ j : Unit,
        (g j : (a : T) → ℝ) (((e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × ((j : Unit) → T)) x).2 j)) ∂μ)
  (∫ (x : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ)
      (∏ i : ι, (f i : (a : X i) → ℝ) (((e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × ((j : Unit) → T)) x).1 i))
      (∏ j : Unit,
        (g j : (a : T) → ℝ) (((e : (a : ((i : ι) → X i) × T) → ((i : ι) → X i) × ((j : Unit) → T)) x).2 j)) ∂ν)
Tactic: rw [integral_map_equiv, integral_map_equiv]
-- 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 : Fintype ι
μ : 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 (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
        (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
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 : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
    (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
  ∫ (p : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((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 : Fintype ι
μ : 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 (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
        (∫ (t : T), (g : (a : T) → ℝ) t ∂ν)
f : (i : ι) → X i →ᵇ ℝ
g : T →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (x : (i : ι) → X i), ∏ i : ι, (f i : (a : X i) → ℝ) (x i) ∂μ)
      (∫ (t : T), (g : (a : T) → ℝ) t ∂ν) =
    ∫ (p : ((i : ι) → X i) × T),
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((g : (a : T) → ℝ) p.2 : ℝ) ∂μ.prod ν
⊢ 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 : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (z.1 i) : ℝ) ((g : (a : T) → ℝ) z.2 : ℝ) ∂μ.prod ν)
  (∫ (p : ((i : ι) → X i) × T),
    HMul.hMul (α := ℝ) (β := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (p.1 i) : ℝ) ((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 : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (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) : ℝ) ∂ν)
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
⊢ μ = ν
have rw : Eq (α := Measure (((i : κ) → Y i) × Z)) (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) μ)
  (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) ν)
Tactic: rw [← e.map_measurableEquiv_injective.eq_iff]
-- 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 : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (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) : ℝ) ∂ν)
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
⊢ Eq (α := Measure (((i : κ) → Y i) × Z)) (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) μ)
    (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) ν)
have refine : ∀ (f : (i : κ) → Y i →ᵇ ℝ) (g : Z →ᵇ ℝ),
  Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) μ)
      fun (p : ((i : κ) → Y i) × Z) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : κ, (f i : (a : Y i) → ℝ) (p.1 i) : ℝ) ((g : (a : Z) → ℝ) p.2 : ℝ))
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) ν)
      fun (p : ((i : κ) → Y i) × Z) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : κ, (f i : (a : Y i) → ℝ) (p.1 i) : ℝ) ((g : (a : Z) → ℝ) 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_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 : Fintype κ
μ ν : Measure (Z × ((j : κ) → Y j))
inst_7 : IsFiniteMeasure μ
inst_8 : IsFiniteMeasure ν
h :
  ∀ (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) : ℝ) ∂ν)
e : Z × ((i : κ) → Y i) ≃ᵐ ((i : κ) → Y i) × Z := MeasurableEquiv.prodComm
f : (i : κ) → Y i →ᵇ ℝ
g : Z →ᵇ ℝ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) μ)
      fun (p : ((i : κ) → Y i) × Z) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : κ, (f i : (a : Y i) → ℝ) (p.1 i) : ℝ) ((g : (a : Z) → ℝ) p.2 : ℝ))
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) ν)
      fun (p : ((i : κ) → Y i) × Z) ↦
      HMul.hMul (α := ℝ) (β := ℝ) (∏ i : κ, (f i : (a : Y i) → ℝ) (p.1 i) : ℝ) ((g : (a : Z) → ℝ) p.2 : ℝ))
have rw : Eq (α := ℝ)
  (∫ (x : Z × ((i : κ) → Y i)),
    HMul.hMul (α := ℝ) (β := ℝ)
      (∏ i : κ, (f i : (a : Y i) → ℝ) (((e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) x).1 i) : ℝ)
      ((g : (a : Z) → ℝ) ((e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) x).2 : ℝ) ∂μ)
  (∫ (x : Z × ((i : κ) → Y i)),
    HMul.hMul (α := ℝ) (β := ℝ)
      (∏ i : κ, (f i : (a : Y i) → ℝ) (((e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) x).1 i) : ℝ)
      ((g : (a : Z) → ℝ) ((e : (a : Z × ((i : κ) → Y i)) → ((i : κ) → Y i) × Z) x).2 : ℝ) ∂ν)
Tactic: rw [integral_map_equiv, integral_map_equiv]
-- 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 : Fintype κ
μ : 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 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ)
        (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν)
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) : ℝ) ∂μ.prod ν)
have rw : HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ)
    (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν) =
  ∫ (p : Z × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ 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_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 : Fintype κ
μ : 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 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂ξ =
      HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ)
        (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν)
f : Z →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
rw :
  HMul.hMul (α := ℝ) (∫ (z : Z), (f : (a : Z) → ℝ) z ∂μ)
      (∫ (y : (j : κ) → Y j), ∏ j : κ, (g j : (a : Y j) → ℝ) (y j) ∂ν) =
    ∫ (p : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (p.2 j) : ℝ) ∂μ.prod ν
⊢ 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) : ℝ) ∂μ.prod ν)
have rw₁ : Eq (α := ℝ)
  (∫ (z : Z × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) z.1 : ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (z.2 j) : ℝ) ∂μ.prod ν)
  (∫ (p : Z × ((j : κ) → Y j)),
    HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) (∏ 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:
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 × T)
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (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 : ℝ) ∂ν)
e : Z × T ≃ᵐ Prod.{u_3, u_4} (Unit → Z) (Unit → T) :=
  MeasurableEquiv.symm (MeasurableEquiv.prodCongr (MeasurableEquiv.funUnique Unit Z) (MeasurableEquiv.funUnique Unit T))
⊢ μ = ν
have rw : Eq (α := Measure (Prod.{u_3, u_4} (Unit → Z) (Unit → T))) (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) μ)
  (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) ν)
Tactic: rw [← e.map_measurableEquiv_injective.eq_iff]
-- 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 × T)
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (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 : ℝ) ∂ν)
e : Z × T ≃ᵐ Prod.{u_3, u_4} (Unit → Z) (Unit → T) :=
  MeasurableEquiv.symm (MeasurableEquiv.prodCongr (MeasurableEquiv.funUnique Unit Z) (MeasurableEquiv.funUnique Unit T))
⊢ Eq (α := Measure (Prod.{u_3, u_4} (Unit → Z) (Unit → T))) (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) μ)
    (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) ν)
have refine : ∀ (f : (i : Unit) → Z →ᵇ ℝ) (g : (j : Unit) → T →ᵇ ℝ),
  Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) μ)
      fun (p : Prod.{u_3, u_4} ((i : Unit) → Z) ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : Unit, (f i : (a : Z) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) ν)
      fun (p : Prod.{u_3, u_4} ((i : Unit) → Z) ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : Unit, (f i : (a : Z) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (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:
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 × T)
inst_6 : IsFiniteMeasure μ
inst_7 : IsFiniteMeasure ν
h :
  ∀ (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 : ℝ) ∂ν)
e : Z × T ≃ᵐ Prod.{u_3, u_4} (Unit → Z) (Unit → T) :=
  MeasurableEquiv.symm (MeasurableEquiv.prodCongr (MeasurableEquiv.funUnique Unit Z) (MeasurableEquiv.funUnique Unit T))
f : (i : Unit) → Z →ᵇ ℝ
g : (j : Unit) → T →ᵇ ℝ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) μ)
      fun (p : Prod.{u_3, u_4} ((i : Unit) → Z) ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : Unit, (f i : (a : Z) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
    (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.map (⇑e : (a : Z × T) → (Unit → Z) × (Unit → T)) ν)
      fun (p : Prod.{u_3, u_4} ((i : Unit) → Z) ((j : Unit) → T)) ↦
      HMul.hMul (α := ℝ) (∏ i : Unit, (f i : (a : Z) → ℝ) (p.1 i)) (∏ j : Unit, (g j : (a : T) → ℝ) (p.2 j)))
have rw : Eq (α := ℝ)
  (∫ (x : Z × T),
    HMul.hMul (α := ℝ)
      (∏ i : Unit, (f i : (a : Z) → ℝ) (((e : (a : Z × T) → ((i : Unit) → Z) × ((j : Unit) → T)) x).1 i))
      (∏ j : Unit, (g j : (a : T) → ℝ) (((e : (a : Z × T) → ((i : Unit) → Z) × ((j : Unit) → T)) x).2 j)) ∂μ)
  (∫ (x : Z × T),
    HMul.hMul (α := ℝ)
      (∏ i : Unit, (f i : (a : Z) → ℝ) (((e : (a : Z × T) → ((i : Unit) → Z) × ((j : Unit) → T)) x).1 i))
      (∏ j : Unit, (g j : (a : T) → ℝ) (((e : (a : Z × T) → ((i : Unit) → Z) × ((j : Unit) → T)) x).2 j)) ∂ν)
Tactic: rw [integral_map_equiv, integral_map_equiv]