α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this : x ∈ EMetric.ball x (ε / 2)
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ Set.Nonempty D ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ Set.Nonempty D ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
have : x ∈ EMetric.ball x (ε / 2) := by
  apply EMetric.mem_ball_self
  rw [ENNReal.div_pos_iff]
  exact ⟨ne_of_gt ε_pos, by norm_num⟩
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ Set.Nonempty D ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this : x ∈ EMetric.ball x (ε / 2)
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ Set.Nonempty D ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
have := hC.closure_nhds_inter x xC this EMetric.isOpen_ball
case refine'_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ closure (EMetric.ball x (ε / 2) ∩ C) ⊆ C

case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (closure (EMetric.ball x (ε / 2) ∩ C)) ≤ ε
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ Set.Nonempty D ∧ D ⊆ C ∧ EMetric.diam D ≤ ε
refine' ⟨this.1, this.2, _, _⟩
case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (EMetric.ball x (ε / 2) ∩ C) ≤ ε
case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (closure (EMetric.ball x (ε / 2) ∩ C)) ≤ ε
rw [EMetric.diam_closure]
case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (EMetric.ball x (ε / 2)) ≤ ε
case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (EMetric.ball x (ε / 2) ∩ C) ≤ ε
apply le_trans (EMetric.diam_mono (inter_subset_left _ _))
case h.e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ ε = 2 * (ε / 2)
case refine'_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.diam (EMetric.ball x (ε / 2)) ≤ ε
convert EMetric.diam_ball (x := x)
no goals
case h.e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ ε = 2 * (ε / 2)
rw [mul_comm, ENNReal.div_mul_cancel] <;> norm_num
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 0 < ε / 2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ x ∈ EMetric.ball x (ε / 2)
apply EMetric.mem_ball_self
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ⊤
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 0 < ε / 2
rw [ENNReal.div_pos_iff]
no goals
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ⊤
exact ⟨ne_of_gt ε_pos, by norm_num⟩
no goals
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 2 ≠ ⊤
norm_num
case refine'_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.ball x (ε / 2) ∩ C ⊆ C
case refine'_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ closure (EMetric.ball x (ε / 2) ∩ C) ⊆ C
rw [IsClosed.closure_subset_iff hC.closed]
no goals
case refine'_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
hC : Perfect C
ε : ℝ≥0∞
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ Set.Nonempty (closure (EMetric.ball x (ε / 2) ∩ C))
⊢ EMetric.ball x (ε / 2) ∩ C ⊆ C
apply inter_subset_right