-- Module: Mathlib.MeasureTheory.Measure.RegularityCompacts
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsCompletelyPseudoMetrizableSpace α
inst_4 : OpensMeasurableSpace α
P : Measure α
inst_5 : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h : Nonempty α
case case₁ case₂ : ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₃ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq), ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₄ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (ht : ∀ (i : ℕ), t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm)
    (h_basis : (𝓤 α).HasAntitoneBasis t), ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₅ case₆ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (h_basis : (𝓤 α).HasAntitoneBasis t) (htu : ∀ (i : ℕ), t i ∈ 𝓤 α)
    (hto : ∀ (i : ℕ), IsOpen (t i)),
    (∀ (i : ℕ), (t i).IsSymm) → ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₇ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (h_basis : (𝓤 α).HasAntitoneBasis t) (htu : ∀ (i : ℕ), t i ∈ 𝓤 α)
    (hto : ∀ (i : ℕ), IsOpen (t i)),
    (∀ (i : ℕ), (t i).IsSymm) →
      let f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n);
      ∀ (h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ),
        ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₈ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (h_basis : (𝓤 α).HasAntitoneBasis t) (htu : ∀ (i : ℕ), t i ∈ 𝓤 α)
    (hto : ∀ (i : ℕ), IsOpen (t i)),
    (∀ (i : ℕ), (t i).IsSymm) →
      let f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n);
      ∀ (h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ)
        (h3 :
          ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε),
            ∃ (m : ℕ), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ m), (f n m')ᶜ) < ε),
        ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₉ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (h_basis : (𝓤 α).HasAntitoneBasis t) (htu : ∀ (i : ℕ), t i ∈ 𝓤 α)
    (hto : ∀ (i : ℕ), IsOpen (t i)),
    (∀ (i : ℕ), (t i).IsSymm) →
      let f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n);
      ∀ (h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ) (s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ)
        (s'bound :
          ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε),
        ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
case₁₀ :
  let seq := denseSeq α;
  ∀ (hseq_dense : DenseRange seq) (t : ℕ → SetRel α α) (h_basis : (𝓤 α).HasAntitoneBasis t) (htu : ∀ (i : ℕ), t i ∈ 𝓤 α)
    (hto : ∀ (i : ℕ), IsOpen (t i)),
    (∀ (i : ℕ), (t i).IsSymm) →
      let f : ℕ → ℕ → Set α := fun (n m : ℕ) ↦ UniformSpace.ball (seq m) (t n);
      ∀ (h_univ : ∀ (n : ℕ), Eq.{u_1 + 1} (α := Set α) (⋃ (m : ℕ), f n m) univ) (s' : (n : ℕ) → (ε : ℝ≥0∞) → ℕ)
        (s'bound :
          ∀ (n : ℕ) (ε : ℝ≥0∞) (hε : 0 < ε), (P : (a : Set α) → ℝ≥0∞) (⋂ (m' : ℕ), ⋂ (_ : m' ≤ s' n ε), (f n m')ᶜ) < ε)
        (δ : ℕ → ℝ≥0∞) (hδ1 : ∀ (i : ℕ), 0 < δ i) (hδ2 : ∑' (i : ℕ), δ i < ε),
        ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε
⊢ ∃ (K : Set α), IsCompact (closure K) ∧ (P : (a : Set α) → ℝ≥0∞) Kᶜ < ε

Tactic:
case inr =>
    let seq := TopologicalSpace.denseSeq α
    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
    obtain ⟨t : ℕ → SetRel α α,
        ht : ∀ i, t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm,
        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
    choose htu hto _ using ht
    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)
    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
      · exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet
      · rw [← compl_iUnion, h_univ, compl_univ]
    choose! s' s'bound using h3
    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
    classical
    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
    rw [interUnionBalls, Set.compl_iInter]
    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
    have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
    simp only [h'', compl_iUnion, ge_iff_le]
    exact (s'bound n (δ n) (hδ1 n)).le

Premises used: Set.compl_iInter, ENNReal.tsum_le_tsum, ENNReal.exists_pos_sum_of_countable', interUnionBalls, ge_iff_le, Filter.HasBasis.exists_antitone_subbasis, ne_of_gt, Set.compl_iUnion, uniformity_hasBasis_open_symmetric, Nat