-- 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 neg.intro.refine_3
Ω : 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 : ℕ
⊢ diam (Bs n) ≤ ε

Tactic:
convert diam_ball half_ε_pos.le

Result:
case h.e'_4
Ω : 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 : ℕ
⊢ ε = 2 * (ε / 2)

Proof state:
case pos.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ ∀ (n : ℕ), diam ((fun x => ∅) n) ≤ ε

Tactic:
intro n

Result:
case pos.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
n : ℕ
⊢ diam ((fun x => ∅) n) ≤ ε

Proof state:
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)

Tactic:
refine ⟨fun _ ↦ ∅, fun _ ↦ MeasurableSet.empty, fun _ ↦ Bornology.isBounded_empty, ?_, ?_,
        fun _ _ _ ↦ disjoint_of_subsingleton⟩

Result:
case pos.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ ∀ (n : ℕ), diam ((fun x => ∅) n) ≤ ε

case pos.refine_2
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
⊢ ⋃ n, (fun x => ∅) n = univ

Proof state:
case pos.refine_1
Ω : Type u_1
inst✝³ : PseudoMetricSpace Ω
inst✝² : MeasurableSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
inst✝ : SeparableSpace Ω
ε : ℝ
ε_pos : 0 < ε
X_emp : IsEmpty Ω
n : ℕ
⊢ diam ((fun x => ∅) n) ≤ ε

Tactic:
simpa only [diam_empty] using LT.lt.le ε_pos

Result:
no goals

Proof state:
case neg.intro.refine_3
Ω : 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 : ℕ
⊢ diam (As n) ≤ ε

Tactic:
apply (diam_mono (disjointed_subset Bs n) isBounded_ball).trans

Result:
case neg.intro.refine_3
Ω : 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 : ℕ
⊢ diam (Bs n) ≤ ε

Proof state:
case neg.intro.refine_4
Ω : 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
aux : ⋃ n, Bs n = univ
⊢ ⋃ n, As n = univ

Tactic:
simpa only [← aux] using iUnion_disjointed

Result:
no goals

Proof state:
case neg.intro.refine_2
Ω : 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 : ℕ), Bornology.IsBounded (As n)

Tactic:
exact fun n ↦ Bornology.IsBounded.subset isBounded_ball <| disjointed_subset Bs n

Result:
no goals

Proof state:
case neg.intro
Ω : 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
⊢ ∃ 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:
refine ⟨As, ?_, ?_, ?_, ?_, ?_⟩

Result:
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)

case neg.intro.refine_2
Ω : 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 : ℕ), Bornology.IsBounded (As n)

case neg.intro.refine_3
Ω : 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 : ℕ), diam (As n) ≤ ε

case neg.intro.refine_4
Ω : 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, As n = univ

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)

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

Tactic:
simp only [univ_eq_empty_iff, X_emp]

Result:
no goals