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)) ∂ν
⊢ μ = ν

Tactic:
by
  have hμν : μ univ = ν univ := by convert! h 1 1 <;> simp
  have : IsFiniteMeasure ν := ⟨by simp [← hμν]⟩
  let π : Set (Set ((Π i, X i) × (Π j, Y j))) :=
    Set.image2 (fun s t ↦ s ×ˢ t) (Set.univ.pi '' (Set.univ.pi fun _ ↦ {s | IsClosed s}))
      (Set.univ.pi '' (Set.univ.pi fun _ ↦ {t | IsClosed t}))
  have hπ1 : IsPiSystem π := by
    rintro - ⟨-, ⟨s₁, hs₁, rfl⟩, -, ⟨t₁, ht₁, rfl⟩, rfl⟩ -
      ⟨-, ⟨s₂, hs₂, rfl⟩, -, ⟨t₂, ht₂, rfl⟩, rfl⟩ -
    refine ⟨_, ⟨fun i ↦ s₁ i ∩ s₂ i, ?_, rfl⟩, _, ⟨fun j ↦ t₁ j ∩ t₂ j, ?_, rfl⟩, ?_⟩
    · simp only [Set.mem_pi, mem_univ, mem_ofPred_eq, forall_const] at hs₁ hs₂ ⊢
      exact fun i ↦ (hs₁ i).inter (hs₂ i)
    · simp only [Set.mem_pi, mem_univ, mem_ofPred_eq, forall_const] at ht₁ ht₂ ⊢
      exact fun j ↦ (ht₁ j).inter (ht₂ j)
    simp [Set.pi_inter_distrib, Set.prod_inter_prod]
  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 _⟩
  refine ext_of_generate_finite π hπ2 hπ1 ?_ hμν
  rintro - ⟨-, ⟨s, hs, rfl⟩, -, ⟨t, ht, rfl⟩, rfl⟩
  simp only [Set.mem_pi, mem_univ, mem_ofPred_eq, forall_const] at hs ht
  have (p : (Π i, X i) × (Π j, Y j)) := ENNReal.continuous_coe.tendsto _ |>.comp <|
    (tendsto_finsetProd Finset.univ (fun i _ ↦ tendsto_pi_nhds.1
      (HasOuterApproxClosed.tendsto_apprSeq (hs i)) (p.1 i))).mul
    (tendsto_finsetProd Finset.univ (fun j _ ↦ tendsto_pi_nhds.1
      (HasOuterApproxClosed.tendsto_apprSeq (ht j)) (p.2 j)))
  have hp1 (x : Π i, X i) : ∏ i, (s i).indicator (fun _ ↦ (1 : ℝ≥0)) (x i) =
      (Set.univ.pi s).indicator 1 x := by
    simp only [Set.indicator, Set.mem_pi, mem_univ, forall_const, Pi.ofNat_apply]
    split_ifs with hy
    · simp only [Set.mem_pi, mem_univ, forall_const] at hy
      exact Finset.prod_eq_one (by simpa)
    · simpa [Finset.prod_eq_zero_iff] using hy
  have hp2 (y : Π j, Y j) : ∏ j, (t j).indicator (fun _ ↦ (1 : ℝ≥0)) (y j) =
      (Set.univ.pi t).indicator 1 y := by
    simp only [Set.indicator, Set.mem_pi, mem_univ, forall_const, Pi.ofNat_apply]
    split_ifs with hy
    · simp only [Set.mem_pi, mem_univ, forall_const] at hy
      exact Finset.prod_eq_one (by simpa)
    · simpa [Finset.prod_eq_zero_iff] using hy
  simp_rw [hp1, hp2, ← Set.indicator_prod_one, Prod.eta] at this
  have h1 : Tendsto (fun n ↦ ∫⁻ p, ((∏ i, (hs i).apprSeq n (p.1 i)) *
        ∏ j, (ht j).apprSeq n (p.2 j) : ℝ≥0) ∂μ)
      atTop (𝓝 (∫⁻ p, (((Set.univ.pi s) ×ˢ (Set.univ.pi t)).indicator 1 p : ℝ≥0) ∂μ)) := by
    refine tendsto_lintegral_filter_of_dominated_convergence 1
      (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun n ↦ ae_of_all _ fun ω ↦ ?_)
      (by simp) (ae_of_all _ this)
    grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)]
    · simp
    · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _
    · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _
  have h2 : Tendsto (fun n ↦ ∫⁻ p, ((∏ i, (hs i).apprSeq n (p.1 i)) *
        ∏ j, (ht j).apprSeq n (p.2 j) : ℝ≥0) ∂μ)
      atTop (𝓝 (∫⁻ p, (((Set.univ.pi s) ×ˢ (Set.univ.pi t)).indicator 1 p : ℝ≥0) ∂ν)) := by
    simp_rw [coe_mul, h]
    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)
    grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)]
    · simp
    · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _
    · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _
  convert! tendsto_nhds_unique h1 h2 <;>
    simp [(MeasurableSet.univ_pi (fun i ↦ (hs i).measurableSet)).prod
      (.univ_pi (fun j ↦ (ht j).measurableSet))]

Goal state after: