-- Mathlib/Topology/MetricSpace/Perfect.lean
theorem Perfect.small_diam_splitting (hC : Perfect C) (hnonempty : C.Nonempty) (ε_pos : 0 < ε) :
    ∃ C₀ C₁ : Set α, (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
    (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))
non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
refine
  ⟨closure (EMetric.ball x₀ (ε / 2) ∩ D₀), closure (EMetric.ball x₁ (ε / 2) ∩ D₁),
    ⟨perf0', non0', sub0'.trans sub0, diam0⟩, ⟨perf1', non1', sub1'.trans sub1, diam1⟩, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))
non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ Disjoint (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
rcases hC.splitting hnonempty with ⟨D₀, D₁, ⟨perf0, non0, sub0⟩, ⟨perf1, non1, sub1⟩, hdisj⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
non0 : D₀.Nonempty
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
non1 : D₁.Nonempty
sub1 : D₁ ⊆ C
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
non0 : D₀.Nonempty
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
non1 : D₁.Nonempty
sub1 : D₁ ⊆ C
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x₀, hx₀⟩ := non0

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
non1 : D₁.Nonempty
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
rcases perf1.small_diam_aux ε_pos hx₁ with ⟨perf1', non1', sub1', diam1⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))
non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ ∃ C₀ C₁,
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ EMetric.diam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ EMetric.diam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (EMetric.ball x₀ (ε / 2) ∩ D₀))
non0' : (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (EMetric.ball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : EMetric.diam (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))
non1' : (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (EMetric.ball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : EMetric.diam (closure (EMetric.ball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ Disjoint (closure (EMetric.ball x₀ (ε / 2) ∩ D₀)) (closure (EMetric.ball x₁ (ε / 2) ∩ D₁))

Tactic:
apply Disjoint.mono _ _ hdisj <;> assumption

Result:
no goals