awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
rw : borel Ω = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s})
    (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s})
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}

Tactic:
rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]

Premises used: borel_eq_generateFrom_isClosed, BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
h₁ :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq_of_IsFiniteMeasure

Premises used: MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
f : Ω →ᵇ ℝ≥0
h₁ :
  (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal = (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν).toReal
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν

Tactic:
apply (ENNReal.toReal_eq_toReal_iff' (lintegral_lt_top_of_nnreal μ f).ne
      (lintegral_lt_top_of_nnreal ν f).ne).mp

Premises used: ENNReal.toReal_eq_toReal_iff', BoundedContinuousFunction.lintegral_lt_top_of_nnreal, Iff.mp, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
f : Ω →ᵇ ℝ≥0
h₁ : Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂ν)
⊢ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal = (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν).toReal

Tactic:
rw [toReal_lintegral_coe_eq_integral f μ, toReal_lintegral_coe_eq_integral f ν]

Premises used: BoundedContinuousFunction.toReal_lintegral_coe_eq_integral
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
f : Ω →ᵇ ℝ≥0
⊢ Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂ν)

Tactic:
h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩,
      f.map_bounded'⟩

Premises used: Continuous.comp', ContinuousMap.mk, NNReal.continuous_coe, BoundedContinuousFunction.continuous, BoundedContinuousFunction.mk, BoundedContinuousFunction.map_bounded', DFunLike.coe, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
f : Ω →ᵇ ℝ≥0
⊢ Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂μ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂ν)

Tactic:
exact h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩,
      f.map_bounded'⟩

Premises used: Continuous.comp', ContinuousMap.mk, NNReal.continuous_coe, BoundedContinuousFunction.continuous, BoundedContinuousFunction.mk, BoundedContinuousFunction.map_bounded', DFunLike.coe, NNReal.toReal
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
⊢ ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν

Tactic:
h 1 1

Premises used: OfNat.ofNat
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
h₁ :
  (μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ =
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ
h₂ :
  (ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ =
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
convert! h 1 1

Premises used: OfNat.ofNat
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
⊢ (μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ =
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ

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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
⊢ (ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ =
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
      (↑(∏ i : ι, ((1 i : X i →ᵇ ℝ≥0) : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) *
        (↑(∏ j : κ, ((1 j : Y j →ᵇ ℝ≥0) : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν

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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have hμν : μ univ = ν univ := by convert! h 1 1 <;> 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [← hμν]
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ IsFiniteMeasure ν

Tactic:
have : IsFiniteMeasure ν := ⟨by simp [← hμν]⟩
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
s₁ : (i : ι) → Set (X i)
hs₁ :
  Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) s₁
t₁ : (i : κ) → Set (Y i)
ht₁ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₁
s₂ : (i : ι) → Set (X i)
hs₂ :
  Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) s₂
t₂ : (i : κ) → Set (Y i)
ht₂ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₂
⊢ (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t) (Set.pi (α := X) univ s₁)
        (Set.pi (α := Y) univ t₁) ∩
      (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t) (Set.pi (α := X) univ s₂)
        (Set.pi (α := Y) univ t₂) ∈
    π

Tactic:
⟨_, ⟨fun i ↦ s₁ i ∩ s₂ i, ?_, rfl⟩, _, ⟨fun j ↦ t₁ j ∩ t₂ j, ?_, rfl⟩, ?_⟩

Premises used: Set.Mem, setOf, Inter.inter, Set.image2, And.intro, Exists.intro, rfl
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
s₁ : (i : ι) → Set (X i)
hs₁ :
  Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) s₁
t₁ : (i : κ) → Set (Y i)
ht₁ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₁
s₂ : (i : ι) → Set (X i)
hs₂ :
  Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) s₂
t₂ : (i : κ) → Set (Y i)
ht₂ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₂
refine_1 :
  ∀ (hs₁ : ∀ (i : ι), IsClosed[inst i] (s₁ i)) (hs₂ : ∀ (i : ι), IsClosed[inst i] (s₂ i)) (i : ι),
    IsClosed[inst i] (s₁ i ∩ s₂ i)
⊢ Membership.mem (γ := Set ((i : ι) → Set (X i)))
    (Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s}) fun (i : ι) ↦
    s₁ i ∩ s₂ i

Tactic:
simp only [Set.mem_pi, mem_univ, mem_setOf_eq, forall_const] at hs₁ hs₂ ⊢

Premises used: Set.mem_pi, Set.mem_setOf_eq, Set.mem_univ, forall_const
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
s₁ : (i : ι) → Set (X i)
t₁ : (i : κ) → Set (Y i)
ht₁ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₁
s₂ : (i : ι) → Set (X i)
t₂ : (i : κ) → Set (Y i)
ht₂ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₂
hs₁ : ∀ (i : ι), IsClosed[inst i] (s₁ i)
hs₂ : ∀ (i : ι), IsClosed[inst i] (s₂ i)
⊢ ∀ (i : ι), IsClosed[inst i] (s₁ i ∩ s₂ i)

Tactic:
fun i ↦ (hs₁ i).inter (hs₂ i)

Premises used: IsClosed.inter
-- 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 : Fintype ι
inst_7 : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst_8 : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
        (↑(∏ i : ι, (f i : (a : X i) → ℝ≥0) (p.1 i)) : ℝ≥0∞) * (↑(∏ j : κ, (g j : (a : Y j) → ℝ≥0) (p.2 j)) : ℝ≥0∞) ∂ν
hμν :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun (s : Set ((i : ι) → X i)) (t : Set ((j : κ) → Y j)) ↦ s ×ˢ t)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})
s₁ : (i : ι) → Set (X i)
t₁ : (i : κ) → Set (Y i)
ht₁ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₁
s₂ : (i : ι) → Set (X i)
t₂ : (i : κ) → Set (Y i)
ht₂ :
  Membership.mem (γ := Set ((i : κ) → Set (Y i)))
    (Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t}) t₂
hs₁ : ∀ (i : ι), IsClosed[inst i] (s₁ i)
hs₂ : ∀ (i : ι), IsClosed[inst i] (s₂ i)
⊢ ∀ (i : ι), IsClosed[inst i] (s₁ i ∩ s₂ i)

Tactic:
exact fun i ↦ (hs₁ i).inter (hs₂ i)

Premises used: IsClosed.inter