awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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:
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:
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))
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)))
⊢ 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:
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:
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 →ᵇ ℝ
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)) ∂ν)
⊢ 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:
rw [integral_map_equiv, integral_map_equiv]

Premises used: MeasureTheory.integral_map_equiv
-- 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))
f : (i : Unit) → Z →ᵇ ℝ
g : (j : Unit) → T →ᵇ ℝ
⊢ 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:
simpa [e] using h (f ()) (g ())

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

Tactic:
rw [h, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- 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 : 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 : ∀ (this : Fintype ι), μ = ν
⊢ μ = ν

Tactic:
have := Fintype.ofFinite ι
-- 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 : 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 : ∀ (this : Fintype κ), μ = ν
⊢ μ = ν

Tactic:
have := Fintype.ofFinite κ
-- 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 : 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 κ
⊢ μ = ν

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
κ : 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 κ
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 ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : 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 κ
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
i : ι
⊢ Continuous[Pi.topologicalSpace, inst i] (Function.eval (β := X) i)

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 : 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 κ
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
j : κ
⊢ Continuous[Pi.topologicalSpace, inst_3 j] (Function.eval (β := Y) j)

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 : 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 κ
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ Eq (α := ℝ) (∏ i : ι, (f i : (a : X i) → ℝ) (x.1 i) : ℝ)
    ((∏ i : ι, (f i).compContinuous { toFun := Function.eval (β := X) i, continuous_toFun := ⋯ } :
          (a : (i : ι) → X i) → ℝ)
        x.1 :
      ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Goal:
ι : Type u_1
κ : Type u_2
X : ι → Type u_5
Y : κ → Type u_6
mX : (i : ι) → MeasurableSpace (X i)
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), BorelSpace.{u_5} (X i)
inst_2 : ∀ (i : ι), HasOuterApproxClosed.{u_5} (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst_3 : (j : κ) → TopologicalSpace (Y j)
inst_4 : ∀ (j : κ), BorelSpace.{u_6} (Y j)
inst_5 : ∀ (j : κ), HasOuterApproxClosed.{u_6} (Y j)
inst_6 : 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 κ
f : (i : ι) → X i →ᵇ ℝ
g : (j : κ) → Y j →ᵇ ℝ
x : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ Eq (α := ℝ) (∏ j : κ, (g j : (a : Y j) → ℝ) (x.2 j) : ℝ)
    ((∏ j : κ, (g j).compContinuous { toFun := Function.eval (β := Y) j, continuous_toFun := ⋯ } :
          (a : (j : κ) → Y j) → ℝ)
        x.2 :
      ℝ)

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 : 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 ν
rw₁ 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 ν)
⊢ 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 ν)

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 : 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 : ∀ (this : Fintype ι), μ = ν
⊢ μ = ν

Tactic:
have := Fintype.ofFinite ι
-- 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 : 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 ι
⊢ μ = ν

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_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 ι
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 ↦ ?_

Premises used: Measure.ext_of_integral_prod_mul_boundedContinuousFunction