-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- In a separable pseudometric space, for any ε > 0 there exists a countable collection of
disjoint Borel measurable subsets of diameter at most ε that cover the whole space. -/
lemma SeparableSpace.exists_measurable_partition_diam_le {ε : ℝ} (ε_pos : 0 < ε) :
    ∃ (As : ℕ → Set Ω), (∀ n, MeasurableSet (As n)) ∧ (∀ n, Bornology.IsBounded (As n)) ∧
        (∀ n, diam (As n) ≤ ε) ∧ (⋃ n, As n = univ) ∧
        (Pairwise (fun (n m : ℕ) ↦ Disjoint (As n) (As m)))

Proof state:
case pos.refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ ∅ = univ

Tactic:
apply Eq.symm

Result:
case pos.refine_2.h
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ univ = ∅

Proof state:
case neg.intro.refine_5
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : ℕ → Set Ω := fun n => ball (xs n) (ε / 2)
As : ℕ → Set Ω := disjointed Bs
⊢ Pairwise fun n m => Disjoint (As n) (As m)

Tactic:
exact disjoint_disjointed Bs

Result:
no goals

Proof state:
case neg.intro.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : ℕ → Set Ω := fun n => ball (xs n) (ε / 2)
As : ℕ → Set Ω := disjointed Bs
⊢ ∀ (n : ℕ), MeasurableSet (As n)

Tactic:
exact MeasurableSet.disjointed (fun n ↦ measurableSet_ball)

Result:
no goals

Proof state:
case neg
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : ¬IsEmpty Ω
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)

Tactic:
rw [not_isEmpty_iff] at X_emp

Result:
case neg
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : Nonempty Ω
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)

Proof state:
case h.e'_2.h.e'_3.h
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : Nonempty Ω
xs : ℕ → Ω
xs_dense : DenseRange xs
half_ε_pos : 0 < ε / 2
Bs : ℕ → Set Ω := fun n => ball (xs n) (ε / 2)
As : ℕ → Set Ω := disjointed Bs
x✝ : ℕ
⊢ Bs x✝ = UniformSpace.ball (xs x✝) {p | dist p.1 p.2 < ε / 2}

Tactic:
exact (ball_eq_ball' _ _).symm

Result:
no goals

Proof state:
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)

Tactic:
by_cases X_emp : IsEmpty Ω

Result:
case pos
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)

case neg
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : ¬IsEmpty Ω
⊢ ∃ As,
    (∀ (n : ℕ), MeasurableSet (As n)) ∧
      (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
        (∀ (n : ℕ), diam (As n) ≤ ε) ∧ ⋃ n, As n = univ ∧ Pairwise fun n m => Disjoint (As n) (As m)