Module: Mathlib.MeasureTheory.Measure.Prokhorov

Goal state before:
pp: case refine_2.inl
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)
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
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : NormalSpace E
⊢ μ (K n)ᶜ ≤ u n

pp: case refine_2.inr
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)
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
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ μ (K n)ᶜ ≤ u n

Tactic:
· -- To show that `μ (Kₙᶜ) ≤ uₙ` when the space is normal, we argue that `μ (Kₙᶜ)` is the
    -- supremum of the integrals of continuous functions supported in `Kₙᶜ` and bounded by `1`,
    -- as the measure is inner regular. Therefore, we are reduced to a question about integrals of
    -- continuous functions, for which we can take advantage of the weak convergence.
    have : Measure.InnerRegular (μ : Measure E) := by simp only [toMeasure_mk, μ]; infer_instance
    rw [← ENNReal.coe_le_coe, ennreal_coeFn_eq_coeFn_toMeasure,
      (hK n).isClosed.isOpen_compl.measure_eq_biSup_integral_continuous]
    simp only [compl_compl, iSup_le_iff, ENNReal.ofReal_le_coe]
    intro g g_cont gK g_nonneg g_le
    have : Tendsto (fun (ρ : FiniteMeasure E) ↦ ∫ x, g x ∂ρ) f (𝓝 (∫ x, g x ∂μ)) := by
      let g' : E →ᵇ ℝ :=
      { toFun := g
        map_bounded' := by
          refine ⟨1, fun x y ↦ ?_⟩
          simp only [dist, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]
          exact ⟨(g_le y).trans (by simpa using g_nonneg x),
            (g_le x).trans (by simpa using g_nonneg y)⟩ }
      exact tendsto_iff_forall_integral_tendsto.1 L g'
    apply le_of_tendsto this
    filter_upwards [hf] with ρ hρ
    calc ∫ x, g x ∂ρ
    _ ≤ ∫ x, indicator (K n)ᶜ 1 x ∂ρ := by
      apply integral_mono_of_nonneg
      · filter_upwards [] with x using g_nonneg x
      · apply Integrable.indicator (integrable_const _) (hK n).measurableSet.compl
      · filter_upwards [] with x
        by_cases hx : x ∈ (K n)ᶜ
        · simpa [hx] using g_le x
        · simp only [hx, not_false_eq_true, indicator_of_notMem]
          apply le_of_eq
          apply gK
          simpa using hx
    _ = ρ (K n)ᶜ := by simp [integral_indicator (hK n).measurableSet.compl]
    _ ≤ u n := mod_cast hρ.2 n

Goal state after:
case refine_2.inr
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)
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
ν : ℕ → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n)).InnerRegular
νK : ∀ (n : ℕ), (ν n) ((partialSups K) n)ᶜ = 0
hν : ∀ (n : ℕ), Tendsto (fun ρ ↦ ρ.restrict (disjointed K n)) (↑f) (𝓝 (ν n))
B : (Measure.sum fun n ↦ ↑(ν n)) univ ≤ ↑C
μ : FiniteMeasure E := ⟨Measure.sum fun n ↦ ↑(ν n), ⋯⟩
L : Tendsto id (↑f) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ μ (K n)ᶜ ≤ u n