Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd

Goal state before:
pp: ι : 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✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun s t ↦ s ×ˢ t) (univ.pi s₁) (univ.pi t₁) ∩ (fun s t ↦ s ×ˢ t) (univ.pi s₂) (univ.pi t₂) ∈ π

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

Goal state after:
case refine_1
ι : 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✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun i ↦ s₁ i ∩ s₂ i) ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}

case refine_2
ι : 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✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun j ↦ t₁ j ∩ t₂ j) ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}

case refine_3
ι : 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✝⁷ : ∀ (i : ι), BorelSpace (X i)
inst✝⁶ : ∀ (i : ι), HasOuterApproxClosed (X i)
mY : (j : κ) → MeasurableSpace (Y j)
inst✝⁵ : (j : κ) → TopologicalSpace (Y j)
inst✝⁴ : ∀ (j : κ), BorelSpace (Y j)
inst✝³ : ∀ (j : κ), HasOuterApproxClosed (Y j)
inst✝² : Fintype ι
inst✝¹ : Fintype κ
μ ν : Measure (((i : ι) → X i) × ((j : κ) → Y j))
inst✝ : IsFiniteMeasure μ
h :
  ∀ (f : (i : ι) → X i →ᵇ ℝ≥0) (g : (j : κ) → Y j →ᵇ ℝ≥0),
    ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂μ =
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (f i) (p.1 i)) * ↑(∏ j, (g j) (p.2 j)) ∂ν
hμν : μ univ = ν univ
this : IsFiniteMeasure ν
π : Set (Set (((i : ι) → X i) × ((j : κ) → Y j))) :=
  image2 (fun s t ↦ s ×ˢ t) (univ.pi '' univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s})
    (univ.pi '' univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t})
s₁ : (i : ι) → Set (X i)
hs₁ : s₁ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₁ : (i : κ) → Set (Y i)
ht₁ : t₁ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
s₂ : (i : ι) → Set (X i)
hs₂ : s₂ ∈ univ.pi fun x ↦ {s | IsClosed[inst✝⁸ x] s}
t₂ : (i : κ) → Set (Y i)
ht₂ : t₂ ∈ univ.pi fun x ↦ {t | IsClosed[inst✝⁵ x] t}
⊢ (fun s t ↦ s ×ˢ t) (univ.pi fun i ↦ s₁ i ∩ s₂ i) (univ.pi fun j ↦ t₁ j ∩ t₂ j) =
    (fun s t ↦ s ×ˢ t) (univ.pi s₁) (univ.pi t₁) ∩ (fun s t ↦ s ×ˢ t) (univ.pi s₂) (univ.pi t₂)