awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
⊢ IsCover ε s s

Tactic:
.rfl

Premises used: SetRel.IsCover.rfl, Metric.IsCover
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
⊢ IsCover ε s s

Tactic:
refl ε s

Premises used: Metric.IsCover.refl
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s N₁ N₂ : Set X
hN : N₁ ⊆ N₂
h₁ : IsCover ε s N₁
⊢ IsCover ε s N₂

Tactic:
h₁.mono hN

Premises used: SetRel.IsCover.mono, Metric.IsCover
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s t N : Set X
hst : s ⊆ t
ht : IsCover ε t N
⊢ IsCover ε s N

Tactic:
ht.anti hst

Premises used: SetRel.IsCover.anti, Metric.IsCover
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy :
  Membership.mem (γ := Set (X × X))
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => edist x y ≤ (↑ε : ENNReal)}
    xy
dsimp : edist xy.1 xy.2 ≤ (↑δ : ENNReal)
⊢ Membership.mem (γ := Set (X × X))
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => edist x y ≤ (↑δ : ENNReal)}
    xy

Tactic:
dsimp at *
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : edist xy.1 xy.2 ≤ (↑ε : ENNReal)
⊢ edist xy.1 xy.2 ≤ (↑δ : ENNReal)

Tactic:
le_trans hxy <| mod_cast hεδ

Premises used: cast, ENNReal.coe_le_coe._simp_1, Eq.symm, le_trans
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε δ : ℝ≥0
s N : Set X
hεδ : ε ≤ δ
hε : IsCover ε s N
xy : X × X
hxy : edist xy.1 xy.2 ≤ (↑ε : ENNReal)
⊢ edist xy.1 xy.2 ≤ (↑δ : ENNReal)

Tactic:
exact le_trans hxy <| mod_cast hεδ

Premises used: le_trans
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
obtain :
  ∀ (x₀ : X) (hx₀ : x₀ ∈ N)
    (hcover :
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (x, x₀)),
    ∃ y ∈ f '' N,
      Membership.mem (γ := SetRel Y Y)
        {x : Y × Y |
          match (motive := Y × Y → Prop) x with
          | (x, y) => edist x y ≤ (↑(K₂ * ε) : ENNReal)}
        (f x, y)
⊢ ∃ y ∈ f '' N,
    Membership.mem (γ := SetRel Y Y)
      {x : Y × Y |
        match (motive := Y × Y → Prop) x with
        | (x, y) => edist x y ≤ (↑(K₂ * ε) : ENNReal)}
      (f x, y)

Tactic:
obtain ⟨x₀, hx₀, hcover⟩ := hs hx
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ (↑ε : ENNReal)
⊢ f x₀ = f x₀

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ (↑ε : ENNReal)
grw : (↑K₂ : ENNReal) * edist x x₀ ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
grw₁ grw₂ : (↑K₂ : ENNReal) * (↑ε : ENNReal) ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
⊢ edist (f x) (f x₀) ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)

Tactic:
grw [hf x x₀, hcover]
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ (↑ε : ENNReal)
⊢ ∃ y ∈ f '' N, edist (f x) y ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)

Tactic:
exact ⟨f x₀, ⟨x₀, hx₀, by grind⟩, by grw [hf x x₀, hcover]⟩
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s : Set Y
N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε (f ⁻¹' s) N
hf : LipschitzWith K₂ f
hf_surj : Function.Surjective f
⊢ IsCover (K₂ * ε) (f '' f ⁻¹' s) (f '' N)

Tactic:
have : IsCover (K₂ * ε) (f '' s.preimage f) (f '' N) := IsCover.image_lipschitz hs hf
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
f : X → Y
s : Set Y
N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε (f ⁻¹' s) N
hf : LipschitzWith K₂ f
hf_surj : Function.Surjective f
this : IsCover (K₂ * ε) (f '' f ⁻¹' s) (f '' N)
⊢ IsCover (K₂ * ε) s (f '' N)

Tactic:
simp_all only [image_preimage_eq]

Premises used: Set.image_preimage_eq
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε s C
⊢ IsCover ε (f '' s) (f '' C)

Tactic:
simpa using h.image_lipschitz hf.lipschitz

Premises used: Isometry.lipschitz, Metric.IsCover.image_lipschitz
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
refine :
  ∀ (h : IsCover ε (f '' s) (f '' C)) (x : X) (hx : x ∈ s),
    ∃ y ∈ C,
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (x, y)
⊢ IsCover ε (f '' s) (f '' C) ↔ IsCover ε s C

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ by simpa using h.image_lipschitz hf.lipschitz⟩
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε (f '' s) (f '' C)
x : X
hx : x ∈ s
obtain :
  ∀ (c : Y) (hc_mem : c ∈ f '' C)
    (hc :
      Membership.mem (γ := SetRel Y Y)
        {x : Y × Y |
          match (motive := Y × Y → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (f x, c)),
    ∃ y ∈ C,
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (x, y)
⊢ ∃ y ∈ C,
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ENNReal)}
      (x, y)

Tactic:
obtain ⟨c, hc_mem, hc⟩ := h (Set.mem_image_of_mem _ hx)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε (f '' s) (f '' C)
x : X
hx : x ∈ s
c : Y
hc_mem : c ∈ f '' C
hc :
  Membership.mem (γ := SetRel Y Y)
    {x : Y × Y |
      match (motive := Y × Y → Prop) x with
      | (x, y) => edist x y ≤ (↑ε : ENNReal)}
    (f x, c)
obtain :
  ∀ (c' : X) (hc' : c' ∈ C)
    (hc :
      Membership.mem (γ := SetRel Y Y)
        {x : Y × Y |
          match (motive := Y × Y → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (f x, f c')),
    ∃ y ∈ C,
      Membership.mem (γ := SetRel X X)
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => edist x y ≤ (↑ε : ENNReal)}
        (x, y)
⊢ ∃ y ∈ C,
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ENNReal)}
      (x, y)

Tactic:
obtain ⟨c', hc', rfl⟩ := hc_mem

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε (f '' s) (f '' C)
x : X
hx : x ∈ s
c' : X
hc' : c' ∈ C
hc :
  Membership.mem (γ := SetRel Y Y)
    {x : Y × Y |
      match (motive := Y × Y → Prop) x with
      | (x, y) => edist x y ≤ (↑ε : ENNReal)}
    (f x, f c')
⊢ ∃ y ∈ C,
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ENNReal)}
      (x, y)

Tactic:
⟨c', hc', le_of_eq_of_le (hf.edist_eq _ _).symm hc⟩

Premises used: Isometry.edist_eq, And.intro, Exists.intro, le_of_eq_of_le, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
ε : ℝ≥0
s : Set X
f : X → Y
hf : Isometry f
C : Set X
h : IsCover ε (f '' s) (f '' C)
x : X
hx : x ∈ s
c' : X
hc' : c' ∈ C
hc :
  Membership.mem (γ := SetRel Y Y)
    {x : Y × Y |
      match (motive := Y × Y → Prop) x with
      | (x, y) => edist x y ≤ (↑ε : ENNReal)}
    (f x, f c')
⊢ ∃ y ∈ C,
    Membership.mem (γ := SetRel X X)
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => edist x y ≤ (↑ε : ENNReal)}
      (x, y)

Tactic:
exact ⟨c', hc', le_of_eq_of_le (hf.edist_eq _ _).symm hc⟩
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
x : X
hA : ediam s ≤ (↑ε : ENNReal)
hx : x ∈ s
x_1 : X
h_mem : x_1 ∈ s
⊢ Membership.mem (γ := Set X) {x} x

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s N : Set X
⊢ IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)

Tactic:
simp [IsCover, SetRel.IsCover, subset_def]

Premises used: Set.subset_def, Metric.IsCover, SetRel.IsCover
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s N : Set X
hN : Maximal (fun (N : Set X) ↦ N ⊆ s ∧ IsSeparated (↑ε : ENNReal) N) N
⊢ Maximal
    (fun (N : Set X) ↦
      N ⊆ s ∧
        SetRel.IsSeparated
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => edist x y ≤ (↑ε : ENNReal)}
          N)
    N

Tactic:
simpa [isSeparated_iff_setRelIsSeparated] using hN

Premises used: Metric.isSeparated_iff_setRelIsSeparated
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : TotallyBounded s
⊢ ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε

Tactic:
rw [EMetric.totallyBounded_iff'] at hs

Premises used: EMetric.totallyBounded_iff'
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
⊢ (↑ε : ENNReal) > 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
obtain :
  ∀ (N : Set X) (hNA : N ⊆ s) (hN_finite : N.Finite) (hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)),
    ∃ N ⊆ s, N.Finite ∧ IsCover ε s N
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
obtain ⟨N, hNA, hN_finite, hN⟩ := hs ε (by positivity)

Premises used: ENNReal.ofNNReal
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
simp : ∃ N ⊆ s, N.Finite ∧ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
simp only [isCover_iff_subset_iUnion_closedEBall]

Premises used: Metric.isCover_iff_subset_iUnion_closedEBall
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
⊢ N ⊆ s

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
⊢ N.Finite

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
refine : s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)
⊢ ∃ N ⊆ s, N.Finite ∧ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)

Tactic:
refine ⟨N, by simpa, by simpa, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
⊢ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)

Tactic:
hN.trans fun x hx ↦ ?_

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
refine :
  ∀ (x : X) (hx : Membership.mem (γ := Set X) (⋃ y ∈ N, eball y (↑ε : ENNReal)) x),
    Membership.mem (γ := Set X) (⋃ y ∈ N, closedEBall y (↑ε : ENNReal)) x
⊢ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)

Tactic:
refine hN.trans fun x hx ↦ ?_

Premises used: HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
x : X
hx : Membership.mem (γ := Set X) (⋃ y ∈ N, eball y (↑ε : ENNReal)) x
simp : ∀ (hx : ∃ i ∈ N, edist x i < (↑ε : ENNReal)), ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)
⊢ Membership.mem (γ := Set X) (⋃ y ∈ N, closedEBall y (↑ε : ENNReal)) x

Tactic:
simp only [Set.mem_iUnion, Metric.mem_eball, exists_prop, Metric.mem_closedEBall] at hx ⊢

Premises used: Metric.mem_closedEBall, Set.mem_iUnion, exists_prop, Metric.mem_eball
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
x : X
hx : ∃ i ∈ N, edist x i < (↑ε : ENNReal)
obtain : ∀ (y : X) (hyN : y ∈ N) (hy : edist x y < (↑ε : ENNReal)), ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)
⊢ ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)

Tactic:
obtain ⟨y, hyN, hy⟩ := hx
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
x y : X
hyN : y ∈ N
hy : edist x y < (↑ε : ENNReal)
⊢ ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)

Tactic:
⟨y, hyN, hy.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
N : Set X
hNA : N ⊆ s
hN_finite : N.Finite
hN : s ⊆ ⋃ y ∈ N, eball y (↑ε : ENNReal)
x y : X
hyN : y ∈ N
hy : edist x y < (↑ε : ENNReal)
⊢ ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)

Tactic:
exact ⟨y, hyN, hy.le⟩
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : IsCompact (closure s)
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
exists_finite_isCover_of_totallyBounded hε (hs.totallyBounded.subset subset_closure)

Premises used: TotallyBounded.subset, subset_closure, IsCompact.totallyBounded, Metric.exists_finite_isCover_of_totallyBounded
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : IsCompact s
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N

Tactic:
exists_finite_isCover_of_totallyBounded hε hs.totallyBounded

Premises used: IsCompact.totallyBounded, Metric.exists_finite_isCover_of_totallyBounded
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
⊢ IsCover ε s N ↔ s ⊆ ⋃ y ∈ N, closedBall y (↑ε : ℝ)

Tactic:
simp [IsCover, SetRel.IsCover, subset_def]

Premises used: Set.subset_def, Metric.IsCover, SetRel.IsCover
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
δ : ℝ≥0
hsN : s ⊆ cthickening (↑ε : ℝ) N
hεδ : ε < δ
⊢ IsCover δ s N

Tactic:
.of_subset_iUnion_closedBall <| hsN.trans (cthickening_subset_iUnion_closedBall_of_lt _
    (NNReal.zero_le_coe.trans_lt hεδ) hεδ)

Premises used: HasSubset.Subset.trans, NNReal.zero_le_coe, LE.le.trans_lt, Metric.cthickening_subset_iUnion_closedBall_of_lt, Metric.IsCover.of_subset_iUnion_closedBall
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst_1 : ProperSpace X
hN : IsClosed N
rw : s ⊆ ⋃ y ∈ N, closedBall y (↑ε : ℝ) ↔ s ⊆ cthickening (↑ε : ℝ) N
rw₁ rw₂ : s ⊆ ⋃ y ∈ N, closedBall y (↑ε : ℝ) ↔ s ⊆ ⋃ x ∈ N, closedBall x (↑ε : ℝ)
⊢ IsCover ε s N ↔ s ⊆ cthickening (↑ε : ℝ) N

Tactic:
rw [isCover_iff_subset_iUnion_closedBall, hN.cthickening_eq_biUnion_closedBall ε.zero_le_coe]

Premises used: IsClosed.cthickening_eq_biUnion_closedBall, Metric.isCover_iff_subset_iUnion_closedBall, NNReal.zero_le_coe
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst_1 : ProperSpace X
hN : IsClosed N
⊢ IsCover ε (closure s) N ↔ IsCover ε s N

Tactic:
simpa [isCover_iff_subset_cthickening hN] using (isClosed_cthickening (E := N)).closure_subset_iff

Premises used: Metric.isCover_iff_subset_cthickening, IsClosed.closure_subset_iff, Metric.isClosed_cthickening
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : EMetricSpace X
s N : Set X
⊢ IsCover 0 s N ↔ s ⊆ N

Tactic:
simp [isCover_iff_subset_iUnion_closedEBall]

Premises used: Metric.isCover_iff_subset_iUnion_closedEBall
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : ProperSpace X
ε : ℝ≥0
s N : Set X
hsN : IsCover ε s N
hs : IsClosed s
hN : IsCompact N
⊢ IsCompact s

Tactic:
.of_isClosed_subset hN.cthickening hs <| hsN.subset_cthickening hN.isClosed

Premises used: IsCompact.cthickening, IsCompact.of_isClosed_subset, Metric.IsCover.subset_cthickening, IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.Cover
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : ProperSpace X
ε : ℝ≥0
s N : Set X
hsN : IsCover ε s N
hN : IsCompact N
⊢ IsCompact (closure s)

Tactic:
(hsN.closure hN.isClosed).isCompact isClosed_closure hN

Premises used: Metric.IsCover.isCompact, isClosed_closure, Metric.IsCover.closure, IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
⊢ externalCoveringNumber.{u_1} (X := X) ε ∅ = 0

Tactic:
simp [externalCoveringNumber]

Premises used: Metric.externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
⊢ coveringNumber.{u_1} (X := X) ε ∅ = 0

Tactic:
simp [coveringNumber]

Premises used: Metric.coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
⊢ packingNumber.{u_1} (X := X) ε ∅ = 0

Tactic:
simp [packingNumber]

Premises used: Metric.packingNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ externalCoveringNumber ε A = 0 ↔ A = ∅

Tactic:
simp [externalCoveringNumber]

Premises used: Metric.externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
rw : ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty
⊢ 0 < externalCoveringNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ coveringNumber ε A = 0 ↔ A = ∅

Tactic:
simp [coveringNumber]

Premises used: Metric.coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
rw : ¬0 < coveringNumber ε A ↔ ¬A.Nonempty
⊢ 0 < coveringNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
simp : (∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅) ↔ A = ∅
⊢ packingNumber ε A = 0 ↔ A = ∅

Tactic:
simp only [packingNumber, ENat.iSup_eq_zero, encard_eq_zero]

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

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
refine : ∀ (h : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅), A = ∅
⊢ (∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅) ↔ A = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- 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) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅
by_contra! : ∀ (this : A.Nonempty), False
⊢ A = ∅

Tactic:
by_contra!
-- 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) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅
this : A.Nonempty
obtain : ∀ (x : X) (hx : x ∈ A), False
⊢ False

Tactic:
obtain ⟨x, hx⟩ := this
-- 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) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅
x : X
hx : x ∈ A
⊢ {x} ⊆ A

Tactic:
simp [hx]
-- 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) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅
x : X
hx : x ∈ A
⊢ IsSeparated (X := X) (↑ε : ℝ≥0∞) {x}

Tactic:
simp
-- 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) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅
x : X
hx : x ∈ A
⊢ False

Tactic:
simpa using h {x} (by simp [hx]) (by simp)

Premises used: Singleton.singleton
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
rw : ¬0 < packingNumber ε A ↔ ¬A.Nonempty
⊢ 0 < packingNumber ε A ↔ A.Nonempty

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty