awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
simp : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsCover ε A i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
⊢ externalCoveringNumber ε A ≤ coveringNumber ε A

Tactic:
simp only [externalCoveringNumber, coveringNumber, le_iInf_iff]

Premises used: le_iInf_iff, Metric.externalCoveringNumber, Metric.coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsCover ε A i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard

Tactic:
fun C _ hC_cover ↦ iInf₂_le C hC_cover

Premises used: iInf₂_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsCover ε A i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard

Tactic:
exact fun C _ hC_cover ↦ iInf₂_le C hC_cover

Premises used: iInf₂_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
hC : IsCover ε A C
⊢ externalCoveringNumber ε A ≤ C.encard

Tactic:
iInf₂_le C hC

Premises used: iInf₂_le, Metric.externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
hC : IsCover ε A C
⊢ coveringNumber ε A ≤ C.encard

Tactic:
(iInf₂_le C h_subset).trans (iInf_le _ hC)

Premises used: iInf₂_le, Metric.coveringNumber, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
hC : IsSeparated (↑ε : ℝ≥0∞) C
⊢ C.encard ≤ packingNumber ε A

Tactic:
le_iSup₂_of_le C h_subset (le_iSup_of_le hC le_rfl)

Premises used: le_rfl, Metric.packingNumber, le_iSup_of_le, le_iSup₂_of_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ IsCover ε A A

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ A ⊆ A

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
simp : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i.encard ≤ A.encard
⊢ packingNumber ε A ≤ A.encard

Tactic:
simp only [packingNumber, iSup_le_iff]

Premises used: Metric.packingNumber, iSup_le_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i.encard ≤ A.encard

Tactic:
fun _ hC _ ↦ encard_le_encard hC

Premises used: Set.encard_le_encard
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i.encard ≤ A.encard

Tactic:
exact fun _ hC _ ↦ encard_le_encard hC

Premises used: Set.encard_le_encard
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
h₁ : ∀ (i : Set X), LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)
⊢ LE.le (α := ℕ∞) (⨅ (C : Set X), ⨅ (_ : IsCover δ A C), C.encard) (⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
i : Set X
⊢ LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)

Tactic:
iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

Premises used: iInf_const_mono, Metric.IsCover.mono_radius
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
i : Set X
⊢ LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)

Tactic:
exact iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

Premises used: iInf_const_mono
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
h₁ : ∀ i ⊆ A, LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)
⊢ LE.le (α := ℕ∞) (⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover δ A C), C.encard)
    (⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
i : Set X
i_1 : i ⊆ A
⊢ LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)

Tactic:
iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

Premises used: iInf_const_mono, Metric.IsCover.mono_radius
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
i : Set X
i_1 : i ⊆ A
⊢ LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)

Tactic:
exact iInf_const_mono (fun h_cover ↦ h_cover.mono_radius h)

Premises used: iInf_const_mono
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
simp : ∀ (i : Set X) (i_1 : IsCover ε B i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
⊢ externalCoveringNumber ε A ≤ externalCoveringNumber ε B

Tactic:
simp only [externalCoveringNumber, le_iInf_iff]

Premises used: le_iInf_iff, Metric.externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ ∀ (i : Set X) (i_1 : IsCover ε B i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard

Tactic:
fun C hC ↦ iInf_le_of_le C <| iInf_le_of_le (hC.anti h) le_rfl

Premises used: le_rfl, Metric.IsCover.anti, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ ∀ (i : Set X) (i_1 : IsCover ε B i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard

Tactic:
exact fun C hC ↦ iInf_le_of_le C <| iInf_le_of_le (hC.anti h) le_rfl

Premises used: le_rfl, iInf_le_of_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A = A.encard

Tactic:
le_antisymm (externalCoveringNumber_le_encard_self A) ?_

Premises used: le_antisymm, Metric.externalCoveringNumber_le_encard_self
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
refine : A.encard ≤ externalCoveringNumber 0 A
⊢ externalCoveringNumber 0 A = A.encard

Tactic:
refine le_antisymm (externalCoveringNumber_le_encard_self A) ?_

Premises used: le_antisymm, Metric.externalCoveringNumber_le_encard_self
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ A.encard ≤ externalCoveringNumber 0 A

Tactic:
le_iInf fun C ↦ le_iInf fun hC₁ ↦ ?_

Premises used: le_iInf, Metric.externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
refine : ∀ (C : Set E) (hC₁ : IsCover 0 A C), A.encard ≤ C.encard
⊢ A.encard ≤ externalCoveringNumber 0 A

Tactic:
refine le_iInf fun C ↦ le_iInf fun hC₁ ↦ ?_

Premises used: le_iInf
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A C : Set E
hC₁ : IsCover 0 A C
⊢ A ⊆ C

Tactic:
rw [isCover_zero] at hC₁

Premises used: Metric.isCover_zero
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard

Tactic:
encard_le_encard hC₁

Premises used: Set.encard_le_encard
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard

Tactic:
exact encard_le_encard hC₁

Premises used: Set.encard_le_encard
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ coveringNumber 0 A = A.encard

Tactic:
le_antisymm (coveringNumber_le_encard_self A) ?_

Premises used: le_antisymm, Metric.coveringNumber_le_encard_self
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
refine : A.encard ≤ coveringNumber 0 A
⊢ coveringNumber 0 A = A.encard

Tactic:
refine le_antisymm (coveringNumber_le_encard_self A) ?_

Premises used: le_antisymm, Metric.coveringNumber_le_encard_self
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
rw : externalCoveringNumber 0 A ≤ coveringNumber 0 A
⊢ A.encard ≤ coveringNumber 0 A

Tactic:
rw [← externalCoveringNumber_zero]

Premises used: Metric.externalCoveringNumber_zero
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A ≤ coveringNumber 0 A

Tactic:
externalCoveringNumber_le_coveringNumber 0 A

Premises used: Metric.externalCoveringNumber_le_coveringNumber, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A ≤ coveringNumber 0 A

Tactic:
exact externalCoveringNumber_le_coveringNumber 0 A

Premises used: Metric.externalCoveringNumber_le_coveringNumber, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ A.encard ≤ ⨆ (_ : A ⊆ A), ⨆ (_ : IsSeparated (↑0 : ℝ≥0∞) A), A.encard

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ coveringNumber ε A = 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
refine_1 : coveringNumber ε A ≤ 1
refine_2 : 1 ≤ coveringNumber ε A
⊢ coveringNumber ε A = 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
refine_1 : ∀ (a : X) (ha : a ∈ A), coveringNumber ε A ≤ 1
⊢ coveringNumber ε A ≤ 1

Tactic:
have ⟨a, ha⟩ := h_nonempty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
a : X
ha : a ∈ A
⊢ {a} ⊆ A

Tactic:
simp [ha]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
a : X
ha : a ∈ A
⊢ encard (α := X) {a} ≤ 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
a : X
ha : a ∈ A
calc : encard (α := X) {a} ≤ 1
⊢ coveringNumber ε A ≤ 1

Tactic:
calc coveringNumber ε A
      _ ≤ ({a} : Set X).encard :=
        (IsCover.singleton_of_ediam_le hA ha).coveringNumber_le_encard (by simp [ha])
      _ ≤ 1 := by simp

Premises used: Set.encard, Metric.IsCover.coveringNumber_le_encard, Metric.coveringNumber, Metric.IsCover.singleton_of_ediam_le, Singleton.singleton
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ 1 ≤ coveringNumber ε A

Tactic:
simpa [Order.one_le_iff_pos]

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ externalCoveringNumber ε A = 1

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
refine_1 : externalCoveringNumber ε A ≤ 1
refine_2 : 1 ≤ externalCoveringNumber ε A
⊢ externalCoveringNumber ε A = 1

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
(externalCoveringNumber_le_coveringNumber ε A).trans_eq
      (coveringNumber_eq_one_of_ediam_le h_nonempty hA)

Premises used: LE.le.trans_eq, Metric.coveringNumber_eq_one_of_ediam_le, Metric.externalCoveringNumber_le_coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
exact (externalCoveringNumber_le_coveringNumber ε A).trans_eq
      (coveringNumber_eq_one_of_ediam_le h_nonempty hA)

Premises used: LE.le.trans_eq, Metric.coveringNumber_eq_one_of_ediam_le, Metric.externalCoveringNumber_le_coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ 1 ≤ externalCoveringNumber ε A

Tactic:
simpa [Order.one_le_iff_pos]

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
inl : ∀ (h_eq_empty : A = ∅), externalCoveringNumber ε A ≤ 1
inr : ∀ (h_nonempty : A.Nonempty), externalCoveringNumber ε A ≤ 1
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : A = ∅
⊢ externalCoveringNumber ε A = 0

Tactic:
rw [← externalCoveringNumber_eq_zero (ε := ε)] at h_eq_empty

Premises used: Metric.externalCoveringNumber_eq_zero
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : externalCoveringNumber ε A = 0
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
simp [h_eq_empty]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_nonempty : A.Nonempty
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
(externalCoveringNumber_eq_one_of_ediam_le h_nonempty hA).le

Premises used: Eq.le, Metric.externalCoveringNumber_eq_one_of_ediam_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_nonempty : A.Nonempty
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
exact (externalCoveringNumber_eq_one_of_ediam_le h_nonempty hA).le

Premises used: Eq.le, Metric.externalCoveringNumber_eq_one_of_ediam_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
inl : ∀ (h_eq_empty : A = ∅), coveringNumber ε A ≤ 1
inr : ∀ (h_nonempty : A.Nonempty), coveringNumber ε A ≤ 1
⊢ coveringNumber ε A ≤ 1

Tactic:
rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : A = ∅
⊢ coveringNumber ε A = 0

Tactic:
rw [← coveringNumber_eq_zero (ε := ε)] at h_eq_empty

Premises used: Metric.coveringNumber_eq_zero
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : coveringNumber ε A = 0
⊢ coveringNumber ε A ≤ 1

Tactic:
simp [h_eq_empty]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_nonempty : A.Nonempty
⊢ coveringNumber ε A ≤ 1

Tactic:
(coveringNumber_eq_one_of_ediam_le h_nonempty hA).le

Premises used: Metric.coveringNumber_eq_one_of_ediam_le, Eq.le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_nonempty : A.Nonempty
⊢ coveringNumber ε A ≤ 1

Tactic:
exact (coveringNumber_eq_one_of_ediam_le h_nonempty hA).le

Premises used: Metric.coveringNumber_eq_one_of_ediam_le, Eq.le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ Set.Nonempty (α := X) {x}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ ediam (X := X) {x} ≤ (↑ε : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ encard (α := X) {x} = 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ Subset (α := Set X) {x} {x}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ IsSeparated (X := X) (↑ε : ℝ≥0∞) {x}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
x : X
⊢ 1 ≤ encard (α := X) {x}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ ∃ (x : Set X) (_ : x ⊆ A) (_ : IsCover ε A x), x.Finite

Tactic:
simp only [coveringNumber, ne_eq, iInf_eq_top, encard_eq_top_iff, not_forall, not_infinite] at h

Premises used: iInf_eq_top, Set.encard_eq_top_iff, ne_eq, Metric.coveringNumber, Set.not_infinite, Classical.not_forall
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ∃ (x : Set X) (_ : x ⊆ A) (_ : IsCover ε A x), x.Finite
obtain :
  ∀ (C' : Set X) (hC'_subset : C' ⊆ A) (hC'_cover : IsCover ε A C') (hC'_fin : C'.Finite),
    ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A

Tactic:
obtain ⟨C', hC'_subset, hC'_cover, hC'_fin⟩ := h
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }

Tactic:
have : Nonempty { s : Set X // s ⊆ A ∧ IsCover ε A s } := ⟨C', hC'_subset, hC'_cover⟩
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
h : ∃ (a : { s : Set X // s ⊆ A ∧ IsCover ε A s }),
  (↑a : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard :=
  ⋯
obtain :
  ∀ (C : { s : Set X // s ⊆ A ∧ IsCover ε A s })
    (hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard),
    ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A

Tactic:
obtain ⟨C, hC⟩ := h
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A

Tactic:
⟨C, C.2.1, ?_, C.2.2, ?_⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
refine_1 : (↑C : Set X).Finite
refine_2 : (↑C : Set X).encard = coveringNumber ε A
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A

Tactic:
refine ⟨C, C.2.1, ?_, C.2.2, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
⊢ (↑C : Set X).Finite

Tactic:
Set.encard_lt_top_iff.mp ?_

Premises used: Set.encard_lt_top_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
refine_1 : (↑C : Set X).encard < ⊤
⊢ (↑C : Set X).Finite

Tactic:
refine Set.encard_lt_top_iff.mp ?_

Premises used: Set.encard_lt_top_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
refine_1 : ∃ (a : Set X), (a ⊆ A ∧ IsCover ε A a) ∧ a.Finite
⊢ (↑C : Set X).encard < ⊤

Tactic:
simp only [hC, iInf_lt_top, encard_lt_top_iff, Subtype.exists, exists_prop]

Premises used: Subtype.exists, Set.encard_lt_top_iff, exists_prop, iInf_lt_top
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
⊢ ∃ (a : Set X), (a ⊆ A ∧ IsCover ε A a) ∧ a.Finite

Tactic:
⟨C', ⟨hC'_subset, hC'_cover⟩, hC'_fin⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsCover ε A s }
C : { s : Set X // s ⊆ A ∧ IsCover ε A s }
hC : (↑C : Set X).encard = ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard
⊢ ∃ (a : Set X), (a ⊆ A ∧ IsCover ε A a) ∧ a.Finite

Tactic:
exact ⟨C', ⟨hC'_subset, hC'_cover⟩, hC'_fin⟩