awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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).encard < ⊤
have refine_1 : ∃ (a : Set X), (a ⊆ A ∧ IsCover ε A a) ∧ a.Finite
Tactic: simp only [hC, iInf_lt_top, encard_lt_top_iff, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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).encard = coveringNumber ε A
have refine_2 : ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard = coveringNumber ε A
Tactic: rw [hC]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ ⨅ (x : { s : Set X // s ⊆ A ∧ IsCover ε A s }), (↑x : Set X).encard = coveringNumber ε A
have refine_2 : ⨅ (i : Set X), ⨅ (_ : i ⊆ A), ⨅ (_ : IsCover ε A i), i.encard = coveringNumber ε A
Tactic: simp_rw [iInf_subtype, iInf_and]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
have inl : ∀ (hA : A = ∅), ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
Tactic: rcases Set.eq_empty_or_nonempty A with hA | hA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
have inr : ∀ (hA : A.Nonempty), ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
Tactic: rcases Set.eq_empty_or_nonempty A with hA | hA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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 }
have obtain : ∀ (a : X) (ha : a ∈ A), Nonempty.{max 1 (u_1 + 1)} { s : Set X // s ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) s }
Tactic: obtain ⟨a, ha⟩ := hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A.Nonempty
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = packingNumber ε A
have this : 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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
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 :=
  ⋯
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
have 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
Tactic: simp_rw [iSup_subtype, iSup_and] at h_exists
Cleared hypotheses: h_exists
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
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
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
have 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
Tactic: specialize h_exists h.lt_top
Cleared hypotheses: h_exists
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ ∃ C ⊆ A,
    C.Finite ∧
      IsSeparated (↑ε : ℝ≥0∞) C ∧ C.encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
have 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
Tactic: obtain ⟨C, hC⟩ := h_exists
Cleared hypotheses: h_exists
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
have inr : (↑C : Set X).Finite
Tactic: refine ⟨C, C.2.1, ?_, C.2.2, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
have inr : (↑C : Set X).encard ≠ ⊤
Tactic: refine Set.encard_ne_top_iff.mp ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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).encard = ⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard
have inr : Eq (α := ℕ∞) (⨆ (i : Set X), ⨆ (_ : i ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) i), i.encard)
  (⨆ (C : Set X), ⨆ (_ : C ⊆ A), ⨆ (_ : IsSeparated (↑ε : ℝ≥0∞) C), C.encard)
Tactic: rw [hC]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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 ≤ (maximalSeparatedSet ε A).encard
have rw : C.encard ≤ packingNumber ε A
Tactic: rw [encard_maximalSeparatedSet h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
x : X
hxA : x ∈ A
⊢ ∃ 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)
have by_contra! : ∀ (h_dist : ∀ (y : X) (_ : y ∈ maximalSeparatedSet ε A), (x, y) ∉ {x : X × X | edist x.1 x.2 ≤ (↑ε : ℝ≥0∞)}), False
Tactic: by_contra! h_dist
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
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
⊢ False
have hx_not_mem : x ∉ maximalSeparatedSet ε A
Tactic: have hx_not_mem : x ∉ maximalSeparatedSet ε A := by simpa using h_dist x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
have refine : ¬C.encard ≤ (maximalSeparatedSet ε A).encard
Tactic: refine absurd (encard_le_of_isSeparated this.1 this.2 h) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ False
have suffices : C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
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)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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 ∧ IsSeparated (↑ε : ℝ≥0∞) C
have left : C ⊆ A
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ C ⊆ A ∧ IsSeparated (↑ε : ℝ≥0∞) C
have right : IsSeparated (↑ε : ℝ≥0∞) C
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A
have 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
Tactic: simp only [packingNumber, ENNReal.coe_mul, ENNReal.coe_ofNat, externalCoveringNumber, le_iInf_iff,
    iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
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)))
      ⋯
⊢ D.encard ≤ C.encard
have hf' : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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∞)
⊢ 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)) : ℕ∞)
have a : Cardinal.mk (↑D : Type u_1) ≤ Cardinal.mk (↑C : Type u_1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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)
have a : ∀ (x y : (↑D : Type u_1)) (hxy : f x = f y), (↑x : X) = (↑y : X)
Tactic: refine Cardinal.mk_le_of_injective (f := f) fun x y hxy ↦ Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ (↑x : X) = (↑y : X)
have a : ¬2 * (↑ε : ℝ≥0∞) < edist (↑x : X) (↑y : X)
Tactic: apply Set.Pairwise.eq hD_separated x.2 y.2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ ¬2 * (↑ε : ℝ≥0∞) < edist (↑x : X) (↑y : X)
have a : edist (↑x : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
Tactic: simp only [not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
have rw : edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)
have h₁ : edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
h₁ : edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
⊢ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)
have h₂ : edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ edist (↑x : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
have edist : edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
Tactic: calc
    edist (x : X) y ≤ edist (x : X) (f x) + edist (f x : X) y := edist_triangle ..
    _ ≤ 2 * ε := by
      rw [two_mul]
      gcongr
      · exact hf' x
      · simpa [edist_comm, hxy] using hf' y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ coveringNumber ε A ≤ packingNumber ε A
have pos : ∀ (h_top : packingNumber ε A ≠ ⊤), coveringNumber ε A ≤ packingNumber ε A
Tactic: by_cases! h_top : packingNumber ε A ≠ ⊤
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
pos : ∀ (h_top : packingNumber ε A ≠ ⊤), coveringNumber ε A ≤ packingNumber ε A
⊢ coveringNumber ε A ≤ packingNumber ε A
have neg : ∀ (h_top : packingNumber ε A = ⊤), coveringNumber ε A ≤ packingNumber ε A
Tactic: by_cases! h_top : packingNumber ε A ≠ ⊤
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A
have pos : coveringNumber ε A ≤ (maximalSeparatedSet ε A).encard
Tactic: rw [← encard_maximalSeparatedSet h_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
have inl : coveringNumber.{u_1} (X := X) (2 * ε) ∅ ≤ externalCoveringNumber.{u_1} (X := X) ε ∅
Tactic: rcases Set.eq_empty_or_nonempty A with rfl | h_nonempty
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
inl : coveringNumber.{u_1} (X := X) (2 * ε) ∅ ≤ externalCoveringNumber.{u_1} (X := X) ε ∅
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
have inr : ∀ (h_nonempty : A.Nonempty), coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
Tactic: rcases Set.eq_empty_or_nonempty A with rfl | h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
have inr : packingNumber (2 * ε) A ≤ externalCoveringNumber ε A
Tactic: refine (coveringNumber_le_packingNumber _ A).trans ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε (f '' A) = coveringNumber ε A
have refine_1 : coveringNumber ε (f '' A) ≤ coveringNumber ε A
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
refine_1 : coveringNumber ε (f '' A) ≤ coveringNumber ε A
⊢ coveringNumber ε (f '' A) = coveringNumber ε A
have refine_2 : coveringNumber ε A ≤ coveringNumber ε (f '' A)
Tactic: refine le_antisymm ?_ ?_