awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) × (Unit → T)
⊢ (fun (p : ((i : ι) → X i) × T) ↦ ((fun (i : ι) ↦ p.1 i, fun (x : Unit) ↦ p.2) : ((i : ι) → X i) × (Unit → T)))
      ((fun (p : ((i : ι) → X i) × (Unit → T)) ↦ ((fun (i : ι) ↦ p.1 i, p.2 ()) : ((i : ι) → X i) × T)) p) =
    p

Tactic:
simp
-- 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 : ℝ) ∂ν)
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 := ⋯ }
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]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.map_measurableEquiv_injective
-- 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 : ℝ) ∂ν)
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)) ν)

Tactic:
ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction
-- 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 : ℝ) ∂ν)
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 := ⋯ }
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)))
⊢ 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:
refine ext_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction
-- 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 : ℝ) ∂ν)
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 →ᵇ ℝ
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)) ∂ν)
⊢ 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:
rw [integral_map_equiv, integral_map_equiv]

Premises used: MeasureTheory.integral_map_equiv
-- 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 : ℝ) ∂ν)
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 (α := ℝ)
    (∫ (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:
simpa [e] using h f (g ())

Premises used: Unit.unit
-- 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)
ν : 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 ν
rw₁ 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 ν)
⊢ 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 ν)

Tactic:
rw [h, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
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]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.map_measurableEquiv_injective
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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) ν)

Tactic:
ext_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_boundedContinuousFunction
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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
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 : ℝ))
⊢ 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:
refine ext_of_integral_prod_mul_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_boundedContinuousFunction
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 →ᵇ ℝ
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 : ℝ) ∂ν)
⊢ 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:
rw [integral_map_equiv, integral_map_equiv]

Premises used: MeasureTheory.integral_map_equiv
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 (α := ℝ)
    (∫ (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:
simpa [e, mul_comm] using h g f

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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 ν
rw₁ 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 ν)
⊢ 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 ν)

Tactic:
rw [h, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
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))
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]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.map_measurableEquiv_injective