-- Module: Mathlib.MeasureTheory.Measure.Portmanteau
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : SecondCountableTopology Ω
S : Set (Set Ω)
ν : ProbabilityMeasure Ω
h : ∀ (u : Set Ω), IsOpen[inst_1] u → ∀ x ∈ u, ∃ s ∈ S, s ∈ 𝓝 x ∧ s ⊆ u
G : Set Ω
hG : IsOpen[inst_1] G
r : ℝ≥0
hr : r < (ν : (a : Set Ω) → ℝ≥0) G
obtain : ∃ T ⊆ S, T.Countable ∧ ⋃ t ∈ T, t = G
obtain₁ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₂ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₃ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₄ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₅ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n)
    (this :
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) (⋃ (i : ℕ), f i)) : Filter ℝ≥0)),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₆ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n)
    (this :
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0)),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
obtain₇ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n)
    (this :
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0))
    (n : ℕ) (hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)),
    ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G
refine_1 :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n)
    (this :
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0))
    (n : ℕ) (hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)),
    r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ Finset.image f (Finset.range (n + 1)), t)
refine_2 refine_2₁ :
  ∀ (T : Set (Set Ω)) (TS : T ⊆ S) (T_count : T.Countable) (hT : ⋃ t ∈ T, t = G) (this : T.Nonempty) (f : ℕ → Set Ω)
    (hf : T = range f) (G_eq : G = ⋃ (n : ℕ), f n)
    (this :
      Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((ν : (a : Set Ω) → ℝ≥0) (accumulate f i) : ℝ≥0)) atTop
        (𝓝 ((ν : (a : Set Ω) → ℝ≥0) G) : Filter ℝ≥0))
    (n : ℕ) (hn : r < (ν : (a : Set Ω) → ℝ≥0) (accumulate f n)), ⋃ t ∈ Finset.image f (Finset.range (n + 1)), t ⊆ G
⊢ ∃ (T : Finset (Set Ω)), (∀ t ∈ T, t ∈ S) ∧ r < (ν : (a : Set Ω) → ℝ≥0) (⋃ t ∈ T, t) ∧ ⋃ t ∈ T, t ⊆ G

Tactic:
classical
  obtain ⟨T, TS, T_count, hT⟩ : ∃ T : Set (Set Ω), T ⊆ S ∧ T.Countable ∧ ⋃ t ∈ T, t = G := by
    have : ∀ (x : G), ∃ s ∈ S, s ∈ 𝓝 (x : Ω) ∧ s ⊆ G := fun x ↦ h G hG x x.2
    choose! s hsS hs_nhds hsG using this
    rcases TopologicalSpace.isOpen_iUnion_countable (fun i ↦ interior (s i))
      (fun i ↦ isOpen_interior) with ⟨T₀, T₀_count, hT₀⟩
    refine ⟨s '' T₀, by grind, T₀_count.image s, ?_⟩
    refine Subset.antisymm (by simp; grind) ?_
    have : G ⊆ ⋃ i, interior (s i) := by
      intro y hy
      simpa using ⟨y, hy, mem_interior_iff_mem_nhds.2 (hs_nhds ⟨y, hy⟩)⟩
    apply this.trans
    rw [← hT₀, biUnion_image]
    exact iUnion₂_mono fun i j ↦ interior_subset
  have : T.Nonempty := by
    contrapose! hr
    simp [← hT, hr]
  rcases T_count.exists_eq_range this with ⟨f, hf⟩
  have G_eq : G = ⋃ n, f n := by simp [← hT, hf]
  have : Tendsto (fun i ↦ ν (accumulate f i)) atTop (𝓝 (ν (⋃ i, f i))) :=
    (ENNReal.tendsto_toNNReal_iff (by simp) (by simp)).2 tendsto_measure_iUnion_accumulate
  rw [← G_eq] at this
  rcases ((tendsto_order.1 this).1 r hr).exists with ⟨n, hn⟩
  refine ⟨(Finset.range (n + 1)).image f, by grind, ?_, ?_⟩
  · convert! hn
    simp [accumulate_def]
  · simpa [G_eq] using fun i _ ↦ subset_iUnion f i

Premises used: Set.accumulate_def, Set