Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
⊢ ∃ x ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}, ↑f ≤ 𝓝 x

Tactic:
have M n : ∃ (ν : FiniteMeasure E), Measure.InnerRegular (ν : Measure E) ∧
      ν (partialSups K n)ᶜ = 0 ∧
      Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f (𝓝 ν) := by
    -- the existence of a limit follows from the fact that these measures are supported in
    -- the compact set `partialSups K n`.
    obtain ⟨ν, hν, ν_lim⟩ : ∃ ν ∈ {ρ : FiniteMeasure E | ρ.mass ≤ C ∧ ρ (partialSups K n)ᶜ = 0},
        Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) f (𝓝 ν) := by
      simp only [Tendsto]
      rw [← Ultrafilter.coe_map]
      apply IsCompact.ultrafilter_le_nhds'
        (isCompact_setOfPred_finiteMeasure_le_of_isCompact C (A n))
      simp only [null_iff_toMeasure_null, Ultrafilter.mem_map, preimage_ofPred_eq]
      filter_upwards [hf] with ρ hρ
      simp only [restrict_mass, restrict_measure_eq,
        Measure.restrict_apply (A n).measurableSet.compl]
      refine ⟨(apply_le_mass ρ _).trans hρ.1, ?_⟩
      convert! measure_empty (μ := (ρ : Measure E))
      apply disjoint_iff.1
      apply disjoint_compl_left.mono_right
      exact le_trans sdiff_le (le_partialSups _ _)
    -- We can find an inner regular measure which coincides with the above limit wrt
    -- integration of bounded continuous functions.
    obtain ⟨ν', ν'_reg, ν'_fin, ν'K, hν'⟩ : ∃ ν', ν'.InnerRegular ∧ IsFiniteMeasure ν' ∧
        ν' (partialSups K n)ᶜ = 0 ∧ ∀ (g : E →ᵇ ℝ), ∫ x, g x ∂ν = ∫ x, g x ∂ν' := by
      apply Measure.exists_innerRegular_eq_of_isCompact _ (A n)
      rw [← MeasureTheory.FiniteMeasure.null_iff_toMeasure_null]
      exact hν.2
    -- This inner regular measure is also a limit for our ultrafilter
    let μ : FiniteMeasure E := ⟨ν', ν'_fin⟩
    refine ⟨μ, ν'_reg, by simp [μ, ν'K], ?_⟩
    apply tendsto_of_forall_integral_tendsto (fun g ↦ ?_)
    convert! tendsto_iff_forall_integral_tendsto.1 ν_lim g using 2
    exact (hν' g).symm

Goal state after:
E : Type u_1
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : T2Space E
inst✝ : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
h : NormalSpace E ∨ Monotone K
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K) n)
A : ∀ (n : ℕ), IsCompact ((partialSups K) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n} ∈ f
M :
  ∀ (n : ℕ),
    ∃ ν, (↑ν).InnerRegular ∧ ν ((partialSups K) n)ᶜ = 0 ∧ Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 ν)
⊢ ∃ x ∈ {μ | μ.mass ≤ C ∧ ∀ (n : ℕ), μ (K n)ᶜ ≤ u n}, ↑f ≤ 𝓝 x