awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
y : X
⊢ Convex ℝ (Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι), ⋂ (_ : y ∈ K i), {r : ℝ≥0∞ | closedEBall y r ⊆ U i})

Tactic:
(convex_Ioi _).inter <| OrdConnected.convex <| OrdConnected.preimage_ennreal_ofReal <|
    ordConnected_iInter fun i => ordConnected_iInter fun (_ : y ∈ K i) =>
      ordConnected_setOf_closedEBall_subset y (U i)

Premises used: Set.ordConnected_iInter, Set.OrdConnected.convex, Metric.ordConnected_setOf_closedEBall_subset, Convex.inter, Set.OrdConnected.preimage_ennreal_ofReal, convex_Ioi
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C(X, ℝ)),
    (∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i

Tactic:
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_comm ι X] using
    exists_continuous_forall_mem_convex_of_local_const exists_forall_closedEBall_subset_aux₂
      (exists_forall_closedEBall_subset_aux₁ hK hU hKU hfin)

Premises used: Metric.exists_forall_closedEBall_subset_aux₂, exists_continuous_forall_mem_convex_of_local_const, Set.mem_inter_iff, Metric.exists_forall_closedEBall_subset_aux₁, forall_comm, Set.mem_iInter, Set.mem_preimage, forall_and
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
rcases :
  ∀ (δ : C(X, ℝ)) (hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ))
    (hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i),
    ∃ (δ : C(X, ℝ≥0)),
      (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
rcases exists_continuous_real_forall_closedEBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩

Premises used: Metric.exists_continuous_real_forall_closedEBall_subset
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i
⊢ ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)

Tactic:
fun x => (hδ₀ x).le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((δ : (a : X) → ℝ) x)) ⊆ U i
lift :
  ∀ (δ : C(X, ℝ≥0)) (hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x : ℝ))
    (hδ :
      ∀ (i : ι),
        ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x)) ⊆ U i),
    ∃ (δ : C(X, ℝ≥0)),
      (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x)) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
⟨δ, hδ₀, fun i x hi => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x)) ⊆ U i
refine : ∀ (i : ι) (x : X) (hi : x ∈ K i), closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
refine ⟨δ, hδ₀, fun i x hi => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x : ℝ)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (ENNReal.ofReal ((ContinuousMap.coeNNRealReal.comp δ : (a : X) → ℝ) x)) ⊆ U i
i : ι
x : X
hi : x ∈ K i
⊢ closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi

Premises used: ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C(X, ℝ≥0∞)),
    (∀ (x : X), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((δ : (a : X) → ℝ≥0∞) x : ℝ≥0∞)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedEBall x ((δ : (a : X) → ℝ≥0∞) x) ⊆ U i

Tactic:
let ⟨δ, hδ₀, hδ⟩ := exists_continuous_nnreal_forall_closedEBall_subset hK hU hKU hfin
  ⟨ContinuousMap.comp ⟨Coe.coe, ENNReal.continuous_coe⟩ δ, fun x => ENNReal.coe_pos.2 (hδ₀ x), hδ⟩

Premises used: Iff.mpr, ContinuousMap.mk, ContinuousMap.comp, Exists, Metric.exists_continuous_nnreal_forall_closedEBall_subset, ENNReal.coe_pos, And, _private.0.Metric.exists_continuous_ennreal_forall_closedEBall_subset.match_1, And.intro, Exists.intro, ENNReal.continuous_coe, Coe.coe
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
rcases :
  ∀ (δ : C(X, ℝ≥0)) (hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0))
    (hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i),
    ∃ (δ : C(X, ℝ≥0)),
      (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        ∀ (i : ι), ∀ x ∈ K i, closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i

Tactic:
rcases Metric.exists_continuous_nnreal_forall_closedEBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩

Premises used: Metric.exists_continuous_nnreal_forall_closedEBall_subset
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i

Tactic:
⟨δ, hδ0, fun i x hx => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
refine : ∀ (i : ι) (x : X) (hx : x ∈ K i), closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i
⊢ ∃ (δ : C(X, ℝ≥0)),
    (∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i

Tactic:
refine ⟨δ, hδ0, fun i x hx => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
i : ι
x : X
hx : x ∈ K i
rw : closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
⊢ closedBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ) ⊆ U i

Tactic:
rw [← Metric.closedEBall_coe]

Premises used: Metric.closedEBall_coe
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
hδ i x hx
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((δ : (a : X) → ℝ≥0) x : ℝ≥0)
hδ : ∀ (i : ι), ∀ x ∈ K i, closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedEBall x (↑((δ : (a : X) → ℝ≥0) x) : ℝ≥0∞) ⊆ U i

Tactic:
exact hδ i x hx
-- Module: Mathlib.Topology.MetricSpace.PartitionOfUnity
Goal:
ι : Type u_1
X : Type u_2
inst : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (K i)
hU : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ (δ : C(X, ℝ)),
    (∀ (x : X), LT.lt (α := ℝ) (0 : ℝ) ((δ : (a : X) → ℝ) x : ℝ)) ∧
      ∀ (i : ι), ∀ x ∈ K i, closedBall x ((δ : (a : X) → ℝ) x) ⊆ U i

Tactic:
let ⟨δ, hδ₀, hδ⟩ := exists_continuous_nnreal_forall_closedBall_subset hK hU hKU hfin
  ⟨ContinuousMap.comp ⟨Coe.coe, NNReal.continuous_coe⟩ δ, hδ₀, hδ⟩

Premises used: Metric.exists_continuous_nnreal_forall_closedBall_subset, ContinuousMap.mk, NNReal.continuous_coe, ContinuousMap.comp, Exists, And, And.intro, Exists.intro, _private.0.Metric.exists_continuous_real_forall_closedBall_subset.match_1, Coe.coe
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
h : 0 < ε / 2
⊢ x ∈ eball x (ε / 2)

Tactic:
apply Metric.mem_eball_self

Premises used: Metric.mem_eball_self
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
h : ε ≠ 0 ∧ Ne (α := ℝ≥0∞) 2 ∞
⊢ 0 < ε / 2

Tactic:
rw [ENNReal.div_pos_iff]

Premises used: ENNReal.div_pos_iff
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
exact ⟨ne_of_gt ε_pos, by simp⟩
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ x ∈ eball x (ε / 2)

Tactic:
have : x ∈ Metric.eball x (ε / 2) := by
    apply Metric.mem_eball_self
    rw [ENNReal.div_pos_iff]
    exact ⟨ne_of_gt ε_pos, by simp⟩
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this : x ∈ eball x (ε / 2)
⊢ Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty

Tactic:
have := hC.closure_nhds_inter x xC this Metric.isOpen_eball
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ let D := closure (eball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ ediam D ≤ ε

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

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
refine_1 : closure (eball x (ε / 2) ∩ C) ⊆ C
refine_2 : ediam (closure (eball x (ε / 2) ∩ C)) ≤ ε
⊢ let D := closure (eball x (ε / 2) ∩ C);
  Perfect D ∧ D.Nonempty ∧ D ⊆ C ∧ ediam D ≤ ε

Tactic:
refine ⟨this.1, this.2, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
refine_1 : eball x (ε / 2) ∩ C ⊆ C
⊢ closure (eball x (ε / 2) ∩ C) ⊆ C

Tactic:
rw [IsClosed.closure_subset_iff hC.closed]

Premises used: Perfect.closed, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ eball x (ε / 2) ∩ C ⊆ C

Tactic:
apply inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
refine_2 : ediam (eball x (ε / 2) ∩ C) ≤ ε
⊢ ediam (closure (eball x (ε / 2) ∩ C)) ≤ ε

Tactic:
rw [Metric.ediam_closure]

Premises used: Metric.ediam_closure
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
refine_2 : ediam (eball x (ε / 2)) ≤ ε
⊢ ediam (eball x (ε / 2) ∩ C) ≤ ε

Tactic:
apply le_trans (Metric.ediam_mono inter_subset_left)

Premises used: Set.inter_subset_left, Metric.ediam_mono, le_trans
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ ediam (eball x (ε / 2)) ≤ 2 * (ε / 2)

Tactic:
Metric.ediam_eball_le (x := x)

Premises used: Metric.ediam_eball_le
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
h : ε = 2 * (ε / 2)
⊢ ediam (eball x (ε / 2)) ≤ ε

Tactic:
convert! Metric.ediam_eball_le (x := x)

Premises used: Metric.ediam_eball_le
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
h : Ne (α := ℝ≥0∞) 2 0
h₁ : Ne (α := ℝ≥0∞) 2 ∞
⊢ ε = 2 * (ε / 2)

Tactic:
rw [mul_comm, ENNReal.div_mul_cancel]

Premises used: ENNReal.div_mul_cancel, mul_comm
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
this_1 : x ∈ eball x (ε / 2)
this : Perfect (closure (eball x (ε / 2) ∩ C)) ∧ (closure (eball x (ε / 2) ∩ C)).Nonempty
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : Type u_1
inst : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
rcases :
  ∀ (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₀ : Set α) (C₁ : Set α),
      (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
        (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁

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

Premises used: Perfect.splitting
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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
obtain :
  ∀ (x₀ : α) (hx₀ : x₀ ∈ D₀),
    ∃ (C₀ : Set α) (C₁ : Set α),
      (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
        (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x₀, hx₀⟩ := non0
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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₀
obtain :
  ∀ (x₁ : α) (hx₁ : x₁ ∈ D₁),
    ∃ (C₀ : Set α) (C₁ : Set α),
      (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
        (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁
⊢ ∃ (C₀ : Set α) (C₁ : Set α),
    (Perfect C₀ ∧ C₀.Nonempty ∧ C₀ ⊆ C ∧ ediam C₀ ≤ ε) ∧
      (Perfect C₁ ∧ C₁.Nonempty ∧ C₁ ⊆ C ∧ ediam C₁ ≤ ε) ∧ Disjoint C₀ C₁

Tactic:
obtain ⟨x₁, hx₁⟩ := non1
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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₁
⊢ Perfect (closure (eball x₀ (ε / 2) ∩ D₀))

Tactic:
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩

Premises used: _private.0.Perfect.small_diam_aux
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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 (eball x₀ (ε / 2) ∩ D₀))
⊢ (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty

Tactic:
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩

Premises used: _private.0.Perfect.small_diam_aux
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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 (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
⊢ closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀

Tactic:
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩

Premises used: _private.0.Perfect.small_diam_aux
-- Module: Mathlib.Topology.MetricSpace.Perfect
Goal:
α : 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 (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
⊢ ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε

Tactic:
rcases perf0.small_diam_aux ε_pos hx₀ with ⟨perf0', non0', sub0', diam0⟩

Premises used: _private.0.Perfect.small_diam_aux