awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard = coveringNumber ε A
⊢ (↑C : Set X).encard = coveringNumber ε A

Tactic:
rw [hC]
-- 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_2 : ⨅ (i : Set X), ⨅ (_ : i ⊆ A), ⨅ (_ : IsCover ε A i), i.encard = coveringNumber ε A
⊢ ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard = coveringNumber ε A

Tactic:
simp_rw [iInf_subtype, iInf_and]

Premises used: iInf_subtype, iInf_and
-- 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
⊢ ⨅ (i : Set X), ⨅ (_ : i ⊆ A), ⨅ (_ : IsCover ε A i), i.encard = coveringNumber ε A

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

Tactic:
grind [minimalCover]

Premises used: Metric.minimalCover
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ (minimalCover ε A).Finite

Tactic:
grind [minimalCover]

Premises used: Metric.minimalCover
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ IsCover ε A (minimalCover ε A)

Tactic:
grind [minimalCover]

Premises used: Metric.minimalCover
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ (minimalCover ε A).encard = coveringNumber ε A

Tactic:
grind [minimalCover]

Premises used: Metric.minimalCover
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
inl : ∀ (hA : A = ∅), ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
inr : ∀ (hA : A.Nonempty), ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A

Tactic:
rcases Set.eq_empty_or_nonempty A with hA | hA

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A = ∅
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A

Tactic:
simp [hA, packingNumber]

Premises used: Metric.packingNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
obtain : ∀ (a : X) (ha : a ∈ A), Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }

Tactic:
obtain ⟨a, ha⟩ := hA
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
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 : packingNumber ε A ≠ ⊤
a : X
ha : a ∈ A
⊢ IsSeparated (X := X) (↑ε : ℝ≥0∞) {a}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
a : X
ha : a ∈ A
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }

Tactic:
exact ⟨⟨{a}, by simp [ha], by simp⟩⟩
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }

Tactic:
have : Nonempty { s : Set X // s ⊆ A ∧ IsSeparated ε s } := by
    obtain ⟨a, ha⟩ := hA
    exact ⟨⟨{a}, by simp [ha], by simp⟩⟩
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
h_exists : ∀ (h : LT.lt (α := ℕ∞) (⨆ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }), (↑i : Set X).encard) ⊤),
  ∃ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }),
    (↑i : Set X).encard = ⨆ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }), (↑i : Set X).encard :=
  ⋯
⊢ ∀ (h : LT.lt (α := ℕ∞) (⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard) ⊤),
    ∃ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }),
      (↑i : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard

Tactic:
simp_rw [iSup_subtype, iSup_and] at h_exists

Premises used: iSup_subtype, iSup_and
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
h_exists :
  ∀ (h : LT.lt (α := ℕ∞) (⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard) ⊤),
    ∃ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }),
      (↑i : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
⊢ ∃ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }),
    (↑i : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard

Tactic:
specialize h_exists h.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
h_exists :
  ∃ (i : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }),
    (↑i : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
inr :
  ∀ (C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s })
    (hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard),
    ∃ C ⊆ A,
      C.Finite ∧
        IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard

Tactic:
obtain ⟨C, hC⟩ := h_exists
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard

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
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
inr : (↑C : Set X).Finite
inr₁ : (↑C : Set X).encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard

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
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
⊢ (↑C : Set X).Finite

Tactic:
Set.encard_ne_top_iff.mp ?_

Premises used: Iff.mp, Set.encard_ne_top_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
inr : (↑C : Set X).encard ≠ ⊤
⊢ (↑C : Set X).Finite

Tactic:
refine Set.encard_ne_top_iff.mp ?_

Premises used: Iff.mp, Set.encard_ne_top_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
inr inr₁ inr₂ inr₃ : Ne (α := ℕ∞) (⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard) ⊤
⊢ (↑C : Set X).encard ≠ ⊤

Tactic:
rwa [hC]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : Ne (α := ℕ∞) (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard) ⊤
hA : A.Nonempty
this : Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
C : { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
hC : (↑C : Set X).encard = ⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard
inr inr₁ :
  Eq (α := ℕ∞) (⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard)
    (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard)
⊢ (↑C : Set X).encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard

Tactic:
rw [hC]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ maximalSeparatedSet ε A ⊆ A

Tactic:
grind [maximalSeparatedSet]

Premises used: Metric.maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ IsSeparated (↑ε : ℝ≥0∞) (maximalSeparatedSet ε A)

Tactic:
grind [maximalSeparatedSet]

Premises used: Metric.maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
⊢ (maximalSeparatedSet ε A).encard = packingNumber ε A

Tactic:
grind [maximalSeparatedSet]

Premises used: Metric.maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε : ℝ≥0∞) C
h : packingNumber ε A ≠ ⊤
rw : C.encard ≤ packingNumber ε A
⊢ C.encard ≤ (maximalSeparatedSet ε A).encard

Tactic:
rw [encard_maximalSeparatedSet h]

Premises used: Metric.encard_maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε : ℝ≥0∞) C
h : packingNumber ε A ≠ ⊤
⊢ C.encard ≤ C.encard

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε : ℝ≥0∞) C
h : packingNumber ε A ≠ ⊤
⊢ C.encard ≤ packingNumber ε A

Tactic:
exact le_iSup_of_le C <| le_iSup_of_le h_subset <| le_iSup_of_le h_sep (by simp)

Premises used: le_iSup_of_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
by_contra! :
  ∀ (h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}), False
⊢ ∃ y ∈ maximalSeparatedSet ε A,
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
      (x, y)

Tactic:
by_contra! h_dist
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
⊢ x ∉ maximalSeparatedSet ε A

Tactic:
simpa using h_dist x
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
⊢ x ∉ maximalSeparatedSet ε A

Tactic:
have hx_not_mem : x ∉ maximalSeparatedSet ε A := by simpa using h_dist x
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
this : C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
⊢ False

Tactic:
absurd (encard_le_of_isSeparated this.1 this.2 h) ?_

Premises used: absurd, And.right, And.left, Metric.encard_le_of_isSeparated
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
this : C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
refine : ¬C.encard ≤ (maximalSeparatedSet ε A).encard
⊢ False

Tactic:
refine absurd (encard_le_of_isSeparated this.1 this.2 h) ?_

Premises used: absurd, And.right, And.left, Metric.encard_le_of_isSeparated
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
this : C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
⊢ ¬C.encard ≤ (maximalSeparatedSet ε A).encard

Tactic:
simp [C, encard_insert_of_notMem hx_not_mem,
      ENat.lt_add_one_iff (encard_maximalSeparatedSet h ▸ h)]

Premises used: ENat.lt_add_one_iff, Set.encard_insert_of_notMem
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
suffices : C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
⊢ False

Tactic:
suffices C ⊆ A ∧ IsSeparated ε C by
    refine absurd (encard_le_of_isSeparated this.1 this.2 h) ?_
    simp [C, encard_insert_of_notMem hx_not_mem,
      ENat.lt_add_one_iff (encard_maximalSeparatedSet h ▸ h)]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
left : C ⊆ A
right : IsSeparated (↑ε : ℝ≥0∞) C
⊢ C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ C ⊆ A

Tactic:
simp [C, hxA, maximalSeparatedSet_subset, Set.insert_subset]

Premises used: Metric.maximalSeparatedSet_subset, Set.insert_subset
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ ∀ y ∈ maximalSeparatedSet ε A, (↑ε : ℝ≥0∞) < edist x y

Tactic:
simpa using h_dist
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}
C : Set X := {x} ∪ maximalSeparatedSet ε A
hx_not_mem : x ∉ maximalSeparatedSet ε A
⊢ IsSeparated (↑ε : ℝ≥0∞) C

Tactic:
exact isSeparated_insert_of_notMem hx_not_mem |>.mpr
      ⟨isSeparated_maximalSeparatedSet, by simpa using h_dist⟩

Premises used: Iff.mpr, Metric.isSeparated_insert_of_notMem, Metric.isSeparated_maximalSeparatedSet, And.intro
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
simp :
  ∀ (i : Set X) (i_1 : IsCover ε A i) (i_2 : Set X) (i_3 : i_2 ⊆ A) (i_4 : IsSeparated (2 * (↑ε : ℝ≥0∞)) i_2),
    i_2.encard ≤ i.encard
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
simp only [packingNumber, ENNReal.coe_mul, ENNReal.coe_ofNat, externalCoveringNumber, le_iInf_iff,
    iSup_le_iff]

Premises used: le_iInf_iff, Metric.externalCoveringNumber, Metric.packingNumber, ENNReal.coe_mul, iSup_le_iff, ENNReal.coe_ofNat
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * (↑ε : ℝ≥0∞)) D
f : (↑D : Type u_1) → (↑C : Type u_1) :=
  fun (x : (↑D : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ C)
      (⋯.choose (p := fun (y : X) ↦
        y ∈ C ∧
          Membership.mem (γ := SetRel X X)
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
⊢ ∀ (x : (↑D : Type u_1)), edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)

Tactic:
have hf' (x : D) : edist x.1 (f x) ≤ ε := (hC_cover (hD_subset x.2)).choose_spec.2
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * (↑ε : ℝ≥0∞)) D
f : (↑D : Type u_1) → (↑C : Type u_1) :=
  fun (x : (↑D : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ C)
      (⋯.choose (p := fun (y : X) ↦
        y ∈ C ∧
          Membership.mem (γ := SetRel X X)
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
hf' : ∀ (x : (↑D : Type u_1)), edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
a : Cardinal.mk (↑D : Type u_1) ≤ Cardinal.mk (↑C : Type u_1)
⊢ LE.le (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Cardinal.mk (↑D : Type u_1)) : ℕ∞)
    ((Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Cardinal.mk (↑C : Type u_1)) : ℕ∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * (↑ε : ℝ≥0∞)) D
f : (↑D : Type u_1) → (↑C : Type u_1) :=
  fun (x : (↑D : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ C)
      (⋯.choose (p := fun (y : X) ↦
        y ∈ C ∧
          Membership.mem (γ := SetRel X X)
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
hf' : ∀ (x : (↑D : Type u_1)), edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
⊢ Cardinal.mk (↑D : Type u_1) ≤ Cardinal.mk (↑C : Type u_1)

Tactic:
Cardinal.mk_le_of_injective (f := f) fun x y hxy ↦ Subtype.ext ?_

Premises used: Cardinal.mk_le_of_injective, Subtype.ext
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * (↑ε : ℝ≥0∞)) D
f : (↑D : Type u_1) → (↑C : Type u_1) :=
  fun (x : (↑D : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ C)
      (⋯.choose (p := fun (y : X) ↦
        y ∈ C ∧
          Membership.mem (γ := SetRel X X)
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
hf' : ∀ (x : (↑D : Type u_1)), edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
a : ∀ (x y : (↑D : Type u_1)) (hxy : f x = f y), (↑x : X) = (↑y : X)
⊢ Cardinal.mk (↑D : Type u_1) ≤ Cardinal.mk (↑C : Type u_1)

Tactic:
refine Cardinal.mk_le_of_injective (f := f) fun x y hxy ↦ Subtype.ext ?_

Premises used: Cardinal.mk_le_of_injective, Subtype.ext
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * (↑ε : ℝ≥0∞)) D
f : (↑D : Type u_1) → (↑C : Type u_1) :=
  fun (x : (↑D : Type u_1)) ↦
    Subtype.mk (p := fun (x : X) ↦ x ∈ C)
      (⋯.choose (p := fun (y : X) ↦
        y ∈ C ∧
          Membership.mem (γ := SetRel X X)
            {x : X × X |
              match (motive := X × X → Prop) x with
              | (x, y) => edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
hf' : ∀ (x : (↑D : Type u_1)), edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
x y : (↑D : Type u_1)
hxy : f x = f y
a : ¬2 * (↑ε : ℝ≥0∞) < edist (↑x : X) (↑y : X)
⊢ (↑x : X) = (↑y : X)

Tactic:
apply Set.Pairwise.eq hD_separated x.2 y.2

Premises used: Set.Pairwise.eq, Subtype.property