awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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})
hπ1 : IsPiSystem π
⊢ ∀ (i : κ), IsCountablySpanning.{u_6} (α := Y i) {t : Set (Y i) | IsClosed[inst_3 i] t}

Tactic:
fun _ ↦ ⟨fun _ ↦ Set.univ, fun _ ↦ isClosed_univ, iUnion_const _⟩

Premises used: isClosed_univ, Set.univ, Set.iUnion_const, And.intro, Exists.intro, IsCountablySpanning
-- 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})
hπ1 : IsPiSystem π
⊢ ∀ (i : κ), IsCountablySpanning.{u_6} (α := Y i) {t : Set (Y i) | IsClosed[inst_3 i] t}

Tactic:
exact fun _ ↦ ⟨fun _ ↦ Set.univ, fun _ ↦ isClosed_univ, iUnion_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})
hπ1 : IsPiSystem π
x : ℕ
⊢ 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 (x : ι) ↦ univ

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∞) ∂ν
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})
hπ1 : IsPiSystem π
x : ℕ
⊢ Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (x : ι) ↦ univ)
    ((fun (x : ℕ) ↦ (univ : Set ((i : ι) → X i))) x)

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∞) ∂ν
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})
hπ1 : IsPiSystem π
⊢ IsCountablySpanning (α := (i : ι) → X i)
    (Set.pi (α := X) univ ''
      Set.pi (α := fun (i : ι) ↦ Set (X i)) univ fun (x : ι) ↦ {s : Set (X x) | IsClosed[inst x] s})

Tactic:
exact ⟨fun _ ↦ Set.univ, fun _ ↦ ⟨fun _ ↦ Set.univ, by simp, by simp⟩, iUnion_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})
hπ1 : IsPiSystem π
x : ℕ
⊢ 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}) fun (x : κ) ↦ univ

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∞) ∂ν
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})
hπ1 : IsPiSystem π
x : ℕ
⊢ Eq (α := Set ((i : κ) → Y i)) (Set.pi (α := Y) univ fun (x : κ) ↦ univ)
    ((fun (x : ℕ) ↦ (univ : Set ((i : κ) → Y i))) x)

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∞) ∂ν
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})
hπ1 : IsPiSystem π
⊢ IsCountablySpanning (α := (i : κ) → Y i)
    (Set.pi (α := Y) univ ''
      Set.pi (α := fun (i : κ) ↦ Set (Y i)) univ fun (x : κ) ↦ {t : Set (Y x) | IsClosed[inst_3 x] t})

Tactic:
exact ⟨fun _ ↦ Set.univ, fun _ ↦ ⟨fun _ ↦ Set.univ, by simp, by simp⟩, iUnion_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})
hπ1 : IsPiSystem π
⊢ Prod.instMeasurableSpace = generateFrom π

Tactic:
have hπ2 : Prod.instMeasurableSpace = generateFrom π := by
    rw [← generateFrom_eq_prod (C := Set.univ.pi '' (Set.univ.pi fun _ ↦ {s | IsClosed s}))
      (D := Set.univ.pi '' (Set.univ.pi fun _ ↦ {t | IsClosed t}))]
    · rw [← generateFrom_eq_pi (C := fun _ ↦ {s | IsClosed s})]
      · simp [BorelSpace.measurable_eq, borel_eq_generateFrom_isClosed]
      · exact fun _ ↦ ⟨fun _ ↦ Set.univ, fun _ ↦ isClosed_univ, iUnion_const _⟩
    · rw [← generateFrom_eq_pi (C := fun _ ↦ {t | IsClosed t})]
      · simp [BorelSpace.measurable_eq, borel_eq_generateFrom_isClosed]
      · exact fun _ ↦ ⟨fun _ ↦ Set.univ, fun _ ↦ isClosed_univ, iUnion_const _⟩
    · exact ⟨fun _ ↦ Set.univ, fun _ ↦ ⟨fun _ ↦ Set.univ, by simp, by simp⟩, iUnion_const _⟩
    · exact ⟨fun _ ↦ Set.univ, fun _ ↦ ⟨fun _ ↦ Set.univ, by simp, by simp⟩, iUnion_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})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
⊢ μ = ν

Tactic:
ext_of_generate_finite π hπ2 hπ1 ?_ hμν

Premises used: MeasureTheory.ext_of_generate_finite
-- 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})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
refine :
  ∀ s ∈ π,
    Eq (α := ℝ≥0∞) ((μ : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν : (a : Set (((i : ι) → X i) × ((j : κ) → Y j))) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
refine ext_of_generate_finite π hπ2 hπ1 ?_ hμν

Premises used: MeasureTheory.ext_of_generate_finite
-- 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})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
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
⊢ ∀ (i : ι), IsClosed[inst i] (s i)

Tactic:
simp only [Set.mem_pi, mem_univ, mem_setOf_eq, forall_const] at hs ht

Premises used: Set.mem_pi, Set.mem_setOf_eq, Set.mem_univ, forall_const