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})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
h1 :
  Tendsto
    (fun n ↦
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑((∏ i, (⋯.apprSeq n) (p.1 i)) * ∏ j, (⋯.apprSeq n) (p.2 j)) ∂μ)
    atTop (𝓝 (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p) ∂μ))
⊢ Tendsto
    (fun n ↦
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑(∏ i, (⋯.apprSeq n) (p.1 i)) * ↑(∏ j, (⋯.apprSeq n) (p.2 j)) ∂ν)
    atTop (𝓝 (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p) ∂ν))

Tactic:
refine tendsto_lintegral_filter_of_dominated_convergence 1
      (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun _ ↦ ae_of_all _ fun _ ↦ ?_)
      (by simp) (ae_of_all _ this)

Goal state after:
ι : 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})
hπ1 : IsPiSystem π
hπ2 : Prod.instMeasurableSpace = generateFrom π
s : (i : ι) → Set (X i)
t : (i : κ) → Set (Y i)
hs : ∀ (i : ι), IsClosed[inst✝⁸ i] (s i)
ht : ∀ (i : κ), IsClosed[inst✝⁵ i] (t i)
hp1 : ∀ (x : (i : ι) → X i), ∏ i, (s i).indicator (fun x ↦ 1) (x i) = (univ.pi s).indicator 1 x
hp2 : ∀ (y : (j : κ) → Y j), ∏ j, (t j).indicator (fun x ↦ 1) (y j) = (univ.pi t).indicator 1 y
this :
  ∀ (p : ((i : ι) → X i) × ((j : κ) → Y j)),
    Tendsto (ofNNReal ∘ fun x ↦ (∏ c, (⋯.apprSeq x) (p.1 c)) * ∏ c, (⋯.apprSeq x) (p.2 c)) atTop
      (𝓝 ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p))
h1 :
  Tendsto
    (fun n ↦
      ∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑((∏ i, (⋯.apprSeq n) (p.1 i)) * ∏ j, (⋯.apprSeq n) (p.2 j)) ∂μ)
    atTop (𝓝 (∫⁻ (p : ((i : ι) → X i) × ((j : κ) → Y j)), ↑((univ.pi s ×ˢ univ.pi t).indicator 1 p) ∂μ))
x✝¹ : ℕ
x✝ : ((i : ι) → X i) × ((j : κ) → Y j)
⊢ ↑(∏ i, (⋯.apprSeq x✝¹) (x✝.1 i)) * ↑(∏ j, (⋯.apprSeq x✝¹) (x✝.2 j)) ≤ 1 x✝