-- Mathlib/Topology/MetricSpace/Perfect.lean
theorem Perfect.small_diam_aux (hC : Perfect C) (ε_pos : 0 < ε) {x : α} (xC : x ∈ C) :
    let D := closure (EMetric.ball x (ε / 2) ∩ C)
    Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Proof state:
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 0 < ε / 2

Tactic:
rw [ENNReal.div_pos_iff]

Result:
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ⊤

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ x ∈ EMetric.ball x (ε / 2)

Tactic:
apply EMetric.mem_ball_self

Result:
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 0 < ε / 2

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this : x ∈ EMetric.ball x (ε / 2)
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Tactic:
have := hC.closure_nhds_inter x xC this EMetric.isOpen_ball

Result:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Tactic:
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⟩

Result:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this : x ∈ EMetric.ball x (ε / 2)
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Proof state:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.ball x (ε / 2) ∩ C ⊆ C

Tactic:
apply inter_subset_right

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (EMetric.ball x (ε / 2)) ≤ ε

Tactic:
convert EMetric.diam_ball (x := x)

Result:
case h.e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ ε = 2 * (ε / 2)

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ let D := closure (EMetric.ball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ EMetric.diam D ≤ ε

Tactic:
refine ⟨this.1, this.2, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ closure (EMetric.ball x (ε / 2) ∩ C) ⊆ C

case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (closure (EMetric.ball x (ε / 2) ∩ C)) ≤ ε

Proof state:
case h.e'_4
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ ε = 2 * (ε / 2)

Tactic:
rw [mul_comm, ENNReal.div_mul_cancel] <;> norm_num

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (closure (EMetric.ball x (ε / 2) ∩ C)) ≤ ε

Tactic:
rw [EMetric.diam_closure]

Result:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (EMetric.ball x (ε / 2) ∩ C) ≤ ε

Proof state:
case h
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ⊤

Tactic:
exact ⟨ne_of_gt ε_pos, by norm_num⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (EMetric.ball x (ε / 2) ∩ C) ≤ ε

Tactic:
apply le_trans (EMetric.diam_mono inter_subset_left)

Result:
case refine_2
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.diam (EMetric.ball x (ε / 2)) ≤ ε

Proof state:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ closure (EMetric.ball x (ε / 2) ∩ C) ⊆ C

Tactic:
rw [IsClosed.closure_subset_iff hC.closed]

Result:
case refine_1
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this✝ : x ∈ EMetric.ball x (ε / 2)
this : Perfect (closure (EMetric.ball x (ε / 2) ∩ C)) ∧ (closure (EMetric.ball x (ε / 2) ∩ C)).Nonempty
⊢ EMetric.ball x (ε / 2) ∩ C ⊆ C

Proof state:
α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ 2 ≠ ⊤

Tactic:
norm_num

Result:
no goals