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

Tactic:
fun_prop
-- 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 ι
f : (i : ι) → X i →ᵇ ℝ
g : T →ᵇ ℝ
h₁ 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 := ⋯ } :
            (a : (i : ι) → X i) → ℝ)
          x.1 :
        ℝ)
⊢ 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:
convert! h (∏ i, (f i).compContinuous ⟨Function.eval i, by fun_prop⟩) g

Premises used: Finset.univ, ContinuousMap.mk, Function.eval, BoundedContinuousFunction.compContinuous, Finset.prod
-- 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 ι
f : (i : ι) → X i →ᵇ ℝ
g : T →ᵇ ℝ
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 := ⋯ } :
          (a : (i : ι) → X i) → ℝ)
        x.1 :
      ℝ)

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

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

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

Tactic:
ext_of_integral_mul_prod_boundedContinuousFunction fun f g ↦ ?_

Premises used: Measure.ext_of_integral_mul_prod_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 : 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 κ
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 ↦ ?_

Premises used: Measure.ext_of_integral_mul_prod_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 : 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 →ᵇ ℝ
j : κ
⊢ Continuous[Pi.topologicalSpace, inst j] (Function.eval (β := Y) j)

Tactic:
fun_prop
-- 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 : 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 →ᵇ ℝ
h₁ 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 := ⋯ } :
            (a : (j : κ) → Y j) → ℝ)
          x.2 :
        ℝ)
⊢ 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:
convert! h f (∏ j, (g j).compContinuous ⟨Function.eval j, by fun_prop⟩)

Premises used: Finset.univ, ContinuousMap.mk, Function.eval, BoundedContinuousFunction.compContinuous, Finset.prod
-- 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 : 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 →ᵇ ℝ
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 := ⋯ } :
          (a : (j : κ) → Y j) → ℝ)
        x.2 :
      ℝ)

Tactic:
simp
-- 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 : 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) →ᵇ ℝ
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 ν
rw₁ rw₂ :
  Eq (α := ℝ)
    (∫ (z : Z × ((j : κ) → Y j)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) z.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) z.2 : ℝ) ∂μ.prod ν)
    (∫ (p : Z × ((i : κ) → Y i)),
      HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : Z) → ℝ) p.1 : ℝ) ((g : (a : (j : κ) → Y j) → ℝ) p.2 : ℝ) ∂μ.prod ν)
⊢ 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 ν)

Tactic:
rw [h, ← integral_prod_mul]

Premises used: MeasureTheory.integral_prod_mul
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
hI :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) ∅ i →
      ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
    (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ i_1 ∈ insert i I, ∀ j ∈ insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)

Tactic:
simp only [Finset.mem_insert] at hI

Premises used: Finset.mem_insert
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
insert : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
insert₁ : AreSeparated (s i) (⋃ x ∈ I, s x)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ Insert.insert i I, s i_1) : ℝ≥0∞)
    (∑ i ∈ Insert.insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]

Premises used: Finset.sum_insert, Finset.set_biUnion_insert
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)

Tactic:
fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ AreSeparated (s i) (⋃ x ∈ I, s x)

Tactic:
Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm

Premises used: Ne.symm, ne_of_mem_of_not_mem, Or.inl, Metric.AreSeparated.finset_iUnion_right, Or.inr, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
s : ι → Set X
i : ι
I : Finset ι
hiI : i ∉ I
ihI :
  ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
hI : ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ I → ∀ (j : ι), j = i ∨ j ∈ I → i_1 ≠ j → AreSeparated (s i_1) (s j)
⊢ ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)

Tactic:
exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]

Premises used: Ne.symm, ne_of_mem_of_not_mem, Or.inl, Metric.AreSeparated.finset_iUnion_right, Or.inr, rfl
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
empty :
  ∀
    (hI :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
      (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
insert :
  ∀ (i : ι) (I : Finset ι) (hiI : i ∉ I)
    (ihI :
      ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞)
          (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞))
    (hI : ∀ i_1 ∈ Insert.insert i I, ∀ j ∈ Insert.insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ Insert.insert i I, s i_1) : ℝ≥0∞)
      (∑ i ∈ Insert.insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]

Premises used: Insert.insert, Finset.mem_insert, Finset.set_biUnion_insert
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
I : Finset ι
s : ι → Set X
hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)
empty :
  ∀
    (hI :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → AreSeparated (s i) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i) : ℝ≥0∞)
      (∑ i ∈ ∅, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
insert :
  ∀ (i : ι) (I : Finset ι) (hiI : i ∉ I)
    (ihI :
      ∀ (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → AreSeparated (s i) (s j)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞)
          (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞))
    (hI : ∀ i_1 ∈ Insert.insert i I, ∀ j ∈ Insert.insert i I, i_1 ≠ j → AreSeparated (s i_1) (s j)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i_1 ∈ Insert.insert i I, s i_1) : ℝ≥0∞)
      (∑ i ∈ Insert.insert i I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (⋃ i ∈ I, s i) : ℝ≥0∞) (∑ i ∈ I, (μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i I hiI ihI =>
    simp only [Finset.mem_insert] at hI
    rw [Finset.set_biUnion_insert, hm, ihI, Finset.sum_insert hiI]
    exacts [fun i hi j hj hij => hI i (Or.inr hi) j (Or.inr hj) hij,
      Metric.AreSeparated.finset_iUnion_right fun j hj =>
        hI i (Or.inl rfl) j (Or.inr hj) (ne_of_mem_of_not_mem hj hiI).symm]

Premises used: Insert.insert, Finset.mem_insert, Finset.set_biUnion_insert
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
rw :
  MeasurableSpace.generateFrom {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤
    μ.caratheodory
⊢ borel X ≤ μ.caratheodory

Tactic:
rw [borel_eq_generateFrom_isClosed]

Premises used: borel_eq_generateFrom_isClosed
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ MeasurableSpace.generateFrom {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤
    μ.caratheodory

Tactic:
MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.isCaratheodory_iff_le, MeasurableSpace.generateFrom_le
-- Module: Mathlib.MeasureTheory.Measure.Hausdorff
Goal:
X : Type u_2
inst : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
refine :
  ∀ (t : Set X)
    (ht :
      Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
        t)
    (s : Set X),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
      (μ : (a : Set X) → ℝ≥0∞) s
⊢ MeasurableSpace.generateFrom {s : Set X | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s} ≤
    μ.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_

Premises used: Iff.mpr, MeasureTheory.OuterMeasure.isCaratheodory_iff_le, MeasurableSpace.generateFrom_le