awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (hypothesis)
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist (f^[n] x) (f^[n] (f x)) ≤ (↑K : ℝ) * dist x (f x)
⊢ IsFixedPt f x
have this₁ : dist x (f x) ≤ (↑K : ℝ) * dist x (f x)
Tactic: rw [← iterate_succ_apply, iterate_succ_apply', hx] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : MetricSpace α
K : ℝ≥0
f : α → α
inst_1 : Nonempty α
inst_2 : CompleteSpace α
n : ℕ
hf : ContractingWith K f^[n]
x : α := fixedPoint f^[n] hf
hx : f^[n] x = x
this : dist x (f x) ≤ (↑K : ℝ) * dist x (f x)
⊢ IsFixedPt f x
have contrapose! : ∀ (this : ¬IsFixedPt f x), (↑K : ℝ) * dist x (f x) < dist x (f x)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ Membership.mem (γ := Set (X × X))
    {x : X × X |
      match (motive := X × X → Prop) x with
      | (x, y) => edist x y ≤ (↑δ : ENNReal)}
    xy
have dsimp : edist xy.1 xy.2 ≤ (↑δ : ENNReal)
Tactic: dsimp at *
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ ∃ 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)
have 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)
Tactic: obtain ⟨x₀, hx₀, hcover⟩ := hs hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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)
⊢ edist (f x) (f x₀) ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
have grw : (↑K₂ : ENNReal) * edist x x₀ ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
Tactic: grw [hf x x₀, hcover]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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)
⊢ edist (f x) (f x₀) ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
have grw₁ : (↑K₂ : ENNReal) * (↑ε : ENNReal) ≤ (↑K₂ : ENNReal) * (↑ε : ENNReal)
Tactic: grw [hf x x₀, hcover]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (hypothesis)
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₂ * ε) s (f '' N)
have this : IsCover (K₂ * ε) (f '' f ⁻¹' s) (f '' N)
Tactic: have : IsCover (K₂ * ε) (f '' s.preimage f) (f '' N) := IsCover.image_lipschitz hs hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ IsCover ε (f '' s) (f '' C) ↔ IsCover ε s C
have 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)
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ by simpa using h.image_lipschitz hf.lipschitz⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ ∃ 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)
have 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)
Tactic: obtain ⟨c, hc_mem, hc⟩ := h (Set.mem_image_of_mem _ hx)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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)
⊢ ∃ 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)
have 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)
Tactic: obtain ⟨c', hc', rfl⟩ := hc_mem
Cleared hypotheses: c, hc_mem, hc
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (hypothesis)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
hε : ε ≠ 0
hs : TotallyBounded s
⊢ ∃ N ⊆ s, N.Finite ∧ IsCover ε s N
have hs₁ : ∀ ε > 0, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, eball y ε
Tactic: rw [EMetric.totallyBounded_iff'] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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 ⊆ s, N.Finite ∧ IsCover ε s N
have 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
Tactic: obtain ⟨N, hNA, hN_finite, hN⟩ := hs ε (by positivity)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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, N.Finite ∧ IsCover ε s N
have simp : ∃ N ⊆ s, N.Finite ∧ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)
Tactic: simp only [isCover_iff_subset_iUnion_closedEBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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, N.Finite ∧ s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)
have refine : s ⊆ ⋃ y ∈ N, closedEBall y (↑ε : ENNReal)
Tactic: refine ⟨N, by simpa, by simpa, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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)
have refine : ∀ (x : X) (hx : Membership.mem (γ := Set X) (⋃ y ∈ N, eball y (↑ε : ENNReal)) x),
  Membership.mem (γ := Set X) (⋃ y ∈ N, closedEBall y (↑ε : ENNReal)) x
Tactic: refine hN.trans fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ Membership.mem (γ := Set X) (⋃ y ∈ N, closedEBall y (↑ε : ENNReal)) x
have simp : ∀ (hx : ∃ i ∈ N, edist x i < (↑ε : ENNReal)), ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)
Tactic: simp only [Set.mem_iUnion, Metric.mem_eball, exists_prop, Metric.mem_closedEBall] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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)
⊢ ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)
have obtain : ∀ (y : X) (hyN : y ∈ N) (hy : edist x y < (↑ε : ENNReal)), ∃ i ∈ N, edist x i ≤ (↑ε : ENNReal)
Tactic: obtain ⟨y, hyN, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ≥0
s N : Set X
inst_1 : ProperSpace X
hN : IsClosed N
⊢ IsCover ε s N ↔ s ⊆ cthickening (↑ε : ℝ) N
have rw : s ⊆ ⋃ y ∈ N, closedBall y (↑ε : ℝ) ↔ s ⊆ cthickening (↑ε : ℝ) N
Tactic: rw [isCover_iff_subset_iUnion_closedBall, hN.cthickening_eq_biUnion_closedBall ε.zero_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Cover (goal)
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
⊢ IsCover ε s N ↔ s ⊆ cthickening (↑ε : ℝ) N
have rw₁ : s ⊆ ⋃ y ∈ N, closedBall y (↑ε : ℝ) ↔ s ⊆ ⋃ x ∈ N, closedBall x (↑ε : ℝ)
Tactic: rw [isCover_iff_subset_iUnion_closedBall, hN.cthickening_eq_biUnion_closedBall ε.zero_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < externalCoveringNumber ε A ↔ A.Nonempty
have rw : ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < coveringNumber ε A ↔ A.Nonempty
have rw : ¬0 < coveringNumber ε A ↔ ¬A.Nonempty
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ packingNumber ε A = 0 ↔ A = ∅
have simp : (∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅) ↔ A = ∅
Tactic: simp only [packingNumber, ENat.iSup_eq_zero, encard_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ (∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅) ↔ A = ∅
have refine : ∀ (h : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i = ∅), A = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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 = ∅
⊢ A = ∅
have by_contra! : ∀ (this : A.Nonempty), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ False
have obtain : ∀ (x : X) (hx : x ∈ A), False
Tactic: obtain ⟨x, hx⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ 0 < packingNumber ε A ↔ A.Nonempty
have rw : ¬0 < packingNumber ε A ↔ ¬A.Nonempty
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ externalCoveringNumber ε A ≤ coveringNumber ε A
have simp : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsCover ε A i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
Tactic: simp only [externalCoveringNumber, coveringNumber, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber ε A ≤ A.encard
have simp : ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsSeparated (↑ε : ℝ≥0∞) i), i.encard ≤ A.encard
Tactic: simp only [packingNumber, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ LE.le (α := ℕ∞) (⨅ (C : Set X), ⨅ (_ : IsCover δ A C), C.encard) (⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard)
have h₁ : ∀ (i : Set X), LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε δ : ℝ≥0
h : ε ≤ δ
⊢ LE.le (α := ℕ∞) (⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover δ A C), C.encard)
    (⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard)
have h₁ : ∀ i ⊆ A, LE.le (α := ℕ∞) (⨅ (_ : IsCover δ A i), i.encard) (⨅ (_ : IsCover ε A i), i.encard)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ externalCoveringNumber ε A ≤ externalCoveringNumber ε B
have simp : ∀ (i : Set X) (i_1 : IsCover ε B i), ⨅ (C : Set X), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
Tactic: simp only [externalCoveringNumber, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ externalCoveringNumber 0 A = A.encard
have refine : A.encard ≤ externalCoveringNumber 0 A
Tactic: refine le_antisymm (externalCoveringNumber_le_encard_self A) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ A.encard ≤ externalCoveringNumber 0 A
have refine : ∀ (C : Set E) (hC₁ : IsCover 0 A C), A.encard ≤ C.encard
Tactic: refine le_iInf fun C ↦ le_iInf fun hC₁ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
Goal:
E : Type u_3
inst : EMetricSpace E
A C : Set E
hC₁ : IsCover 0 A C
⊢ A.encard ≤ C.encard
have hC₂ : A ⊆ C
Tactic: rw [isCover_zero] at hC₁
Cleared hypotheses: hC₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ coveringNumber 0 A = A.encard
have refine : A.encard ≤ coveringNumber 0 A
Tactic: refine le_antisymm (coveringNumber_le_encard_self A) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
E : Type u_3
inst : EMetricSpace E
A : Set E
⊢ A.encard ≤ coveringNumber 0 A
have rw : externalCoveringNumber 0 A ≤ coveringNumber 0 A
Tactic: rw [← externalCoveringNumber_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ coveringNumber ε A = 1
have refine_1 : coveringNumber ε A ≤ 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ coveringNumber ε A = 1
have refine_2 : 1 ≤ coveringNumber ε A
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ coveringNumber ε A ≤ 1
have refine_1 : ∀ (a : X) (ha : a ∈ A), coveringNumber ε A ≤ 1
Tactic: have ⟨a, ha⟩ := h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ coveringNumber ε A ≤ 1
have calc : encard (α := X) {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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ externalCoveringNumber ε A = 1
have refine_1 : externalCoveringNumber ε A ≤ 1
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
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
⊢ externalCoveringNumber ε A = 1
have refine_2 : 1 ≤ externalCoveringNumber ε A
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ externalCoveringNumber ε A ≤ 1
have inl : ∀ (h_eq_empty : A = ∅), externalCoveringNumber ε A ≤ 1
Tactic: rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
inl : ∀ (h_eq_empty : A = ∅), externalCoveringNumber ε A ≤ 1
⊢ externalCoveringNumber ε A ≤ 1
have inr : ∀ (h_nonempty : A.Nonempty), externalCoveringNumber ε A ≤ 1
Tactic: rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : A = ∅
⊢ externalCoveringNumber ε A ≤ 1
have h_eq_empty₁ : externalCoveringNumber ε A = 0
Tactic: rw [← externalCoveringNumber_eq_zero (ε := ε)] at h_eq_empty
Cleared hypotheses: h_eq_empty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
⊢ coveringNumber ε A ≤ 1
have inl : ∀ (h_eq_empty : A = ∅), coveringNumber ε A ≤ 1
Tactic: rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
inl : ∀ (h_eq_empty : A = ∅), coveringNumber ε A ≤ 1
⊢ coveringNumber ε A ≤ 1
have inr : ∀ (h_nonempty : A.Nonempty), coveringNumber ε A ≤ 1
Tactic: rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ (↑ε : ℝ≥0∞)
h_eq_empty : A = ∅
⊢ coveringNumber ε A ≤ 1
have h_eq_empty₁ : coveringNumber ε A = 0
Tactic: rw [← coveringNumber_eq_zero (ε := ε)] at h_eq_empty
Cleared hypotheses: h_eq_empty
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : coveringNumber ε A ≠ ⊤
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : ∃ (x : Set X) (_ : x ⊆ A) (_ : IsCover ε A x), x.Finite
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have 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
Tactic: obtain ⟨C', hC'_subset, hC'_cover, hC'_fin⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.CoveringNumbers (hypothesis)
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
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have this : 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⟩
-- 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 }
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 :=
  ⋯
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have 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
Tactic: obtain ⟨C, hC⟩ := h
Cleared hypotheses: h
-- 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 ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have refine_1 : (↑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
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
⊢ ∃ C ⊆ A, C.Finite ∧ IsCover ε A C ∧ C.encard = coveringNumber ε A
have refine_2 : (↑C : Set X).encard = coveringNumber ε A
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
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
have refine_1 : (↑C : Set X).encard < ⊤
Tactic: refine Set.encard_lt_top_iff.mp ?_