awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : edist (↑x : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
⊢ ¬2 * (↑ε : ℝ≥0∞) < edist (↑x : X) (↑y : X)

Tactic:
simp only [not_lt]

Premises used: not_lt
-- 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
⊢ edist (↑x : X) (↑y : X) ≤ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X)

Tactic:
edist_triangle ..

Premises used: PseudoEMetricSpace.edist_triangle
-- 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
rw : edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)
⊢ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)

Tactic:
rw [two_mul]

Premises used: two_mul
-- 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
h₁ : edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
h₂ : edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞)
⊢ edist (↑x : X) (↑(f x) : X) + edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)

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∞)
x y : (↑D : Type u_1)
hxy : f x = f y
⊢ edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)

Tactic:
hf' x
-- 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
⊢ edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)

Tactic:
exact hf' x
-- 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
⊢ edist (↑(f x) : X) (↑y : X) ≤ (↑ε : ℝ≥0∞)

Tactic:
simpa [edist_comm, hxy] using hf' y

Premises used: PseudoEMetricSpace.edist_comm
-- 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.edist x y ≤ (↑ε : ℝ≥0∞)}
            ((↑x : X), y)))
      ⋯
hf' : ∀ (x : (↑D : Type u_1)), EDist.edist (↑x : X) (↑(f x) : X) ≤ (↑ε : ℝ≥0∞)
x y : (↑D : Type u_1)
hxy : f x = f y
edist : EDist.edist (↑x : X) (↑(f x) : X) + EDist.edist (↑(f x) : X) (↑y : X) ≤ 2 * (↑ε : ℝ≥0∞)
⊢ EDist.edist (↑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

Premises used: EDist.edist, Subtype.val, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
pos : ∀ (h_top : packingNumber ε A ≠ ⊤), coveringNumber ε A ≤ packingNumber ε A
neg : ∀ (h_top : packingNumber ε A = ⊤), coveringNumber ε A ≤ packingNumber ε A
⊢ coveringNumber ε A ≤ packingNumber ε A

Tactic:
by_cases! h_top : packingNumber ε A ≠ ⊤

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

Tactic:
rw [← encard_maximalSeparatedSet h_top]

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

Tactic:
isCover_maximalSeparatedSet h_top |>.coveringNumber_le_encard maximalSeparatedSet_subset

Premises used: Metric.maximalSeparatedSet_subset, Metric.IsCover.coveringNumber_le_encard, Metric.isCover_maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A ≠ ⊤
⊢ coveringNumber ε A ≤ (maximalSeparatedSet ε A).encard

Tactic:
exact isCover_maximalSeparatedSet h_top |>.coveringNumber_le_encard maximalSeparatedSet_subset

Premises used: Metric.maximalSeparatedSet_subset, Metric.IsCover.coveringNumber_le_encard, Metric.isCover_maximalSeparatedSet
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_top : packingNumber ε A = ⊤
⊢ coveringNumber ε A ≤ packingNumber ε A

Tactic:
simp [h_top]
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
inl : coveringNumber.{u_1} (X := X) (2 * ε) ∅ ≤ externalCoveringNumber.{u_1} (X := X) ε ∅
inr : ∀ (h_nonempty : A.Nonempty), coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
rcases Set.eq_empty_or_nonempty A with rfl | h_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
⊢ coveringNumber.{u_1} (X := X) (2 * ε) ∅ ≤ externalCoveringNumber.{u_1} (X := X) ε ∅

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
(coveringNumber_le_packingNumber _ A).trans ?_

Premises used: Metric.coveringNumber_le_packingNumber, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
inr : packingNumber (2 * ε) A ≤ externalCoveringNumber ε A
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
refine (coveringNumber_le_packingNumber _ A).trans ?_

Premises used: Metric.coveringNumber_le_packingNumber, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
packingNumber_two_mul_le_externalCoveringNumber ε A

Premises used: Metric.packingNumber_two_mul_le_externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
h_nonempty : A.Nonempty
⊢ packingNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
exact packingNumber_two_mul_le_externalCoveringNumber ε A

Premises used: Metric.packingNumber_two_mul_le_externalCoveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
A B : Set X
ε : ℝ≥0
h : A ⊆ B
⊢ packingNumber ε A = packingNumber (2 * (ε / 2)) A

Tactic:
ring_nf
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
refine_2 : coveringNumber ε A ≤ coveringNumber ε (f '' A)
⊢ coveringNumber ε (f '' A) = coveringNumber ε A

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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 :
  ∀ (i : Set X) (i_1 : i ⊆ A) (i_2 : IsCover ε A i),
    ⨅ (C : Set Y), ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ i.encard
⊢ coveringNumber ε (f '' A) ≤ coveringNumber ε A

Tactic:
simp only [coveringNumber, le_iInf_iff]

Premises used: le_iInf_iff, Metric.coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
⊢ ⨅ (C : Set Y), ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ C.encard

Tactic:
(iInf_le _ (C.image f)).trans ?_

Premises used: Set.image, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
refine_1 : ⨅ (_ : f '' C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard
⊢ ⨅ (C : Set Y), ⨅ (_ : C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) C), C.encard ≤ C.encard

Tactic:
refine (iInf_le _ (C.image f)).trans ?_

Premises used: Set.image, LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
refine_1 : ⨅ (_ : C ⊆ f ⁻¹' f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard
⊢ ⨅ (_ : f '' C ⊆ f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
simp only [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
⊢ C ⊆ f ⁻¹' f '' A

Tactic:
have : ↑C ⊆ f ⁻¹' f '' A := hC_subset.trans (Set.subset_preimage_image f A)
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ ⨅ (_ : C ⊆ f ⁻¹' f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
(iInf_le _ this).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
refine_1 : ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard
⊢ ⨅ (_ : C ⊆ f ⁻¹' f '' A), ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
refine (iInf_le _ this).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
refine_1 : ⨅ (_ : IsCover ε A C), (f '' C).encard ≤ C.encard
⊢ ⨅ (_ : IsCover ε (f '' A) (f '' C)), (f '' C).encard ≤ C.encard

Tactic:
rw [hf.isCover_image_iff]

Premises used: Isometry.isCover_image_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ ⨅ (_ : IsCover ε A C), (f '' C).encard ≤ C.encard

Tactic:
(iInf_le _ hC_cover).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
refine_1 : (f '' C).encard ≤ C.encard
⊢ ⨅ (_ : IsCover ε A C), (f '' C).encard ≤ C.encard

Tactic:
refine (iInf_le _ hC_cover).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ (f '' C).encard ≤ C.encard

Tactic:
encard_image_le f C

Premises used: Set.encard_image_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set X
hC_subset : C ⊆ A
hC_cover : IsCover ε A C
this : C ⊆ f ⁻¹' f '' A
⊢ (f '' C).encard ≤ C.encard

Tactic:
exact encard_image_le f C

Premises used: Set.encard_image_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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_2 :
  ∀ (i : Set Y) (i_1 : i ⊆ f '' A) (i_2 : IsCover ε (f '' A) i),
    ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ i.encard
⊢ coveringNumber ε A ≤ coveringNumber ε (f '' A)

Tactic:
simp only [coveringNumber, le_iInf_iff]

Premises used: le_iInf_iff, Metric.coveringNumber
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
x : (↑C : Type u_2)
⊢ ∃ y ∈ A, f y = (↑x : Y)

Tactic:
simpa using hC_subset x.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
⊢ ∀ (x : (↑C : Type u_2)), ∃ y ∈ A, f y = (↑x : Y)

Tactic:
have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
this : ∀ (x : (↑C : Type u_2)), ∃ y ∈ A, f y = (↑x : Y)
choose :
  ∀ (g : (x : (↑C : Type u_2)) → X) (hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A)
    (hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)), ∃ C' ⊆ A, C = f '' C'
⊢ ∃ C' ⊆ A, C = f '' C'

Tactic:
choose g hg_mem hg using this
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
⊢ ∃ C' ⊆ A, C = f '' C'

Tactic:
⟨Set.range g, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Set.range
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
refine_1 : range g ⊆ A
refine_2 : C = f '' range g
⊢ ∃ C' ⊆ A, C = f '' C'

Tactic:
refine ⟨Set.range g, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (y : (↑C : Type u_2)), g y ∈ A
⊢ range g ⊆ A

Tactic:
rwa [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
refine_2 : ∀ (x : Y), x ∈ C ↔ x ∈ f '' range g
⊢ C = f '' range g

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
x : Y
refine_2 : x ∈ C ↔ ∃ (a : Y) (h : a ∈ C), f (g (Subtype.mk (p := fun (a : Y) ↦ a ∈ C) a ⋯)) = x
⊢ x ∈ C ↔ x ∈ f '' range g

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : (x : (↑C : Type u_2)) → X
hg_mem : ∀ (x : (↑C : Type u_2)), g x ∈ A
hg : ∀ (x : (↑C : Type u_2)), f (g x) = (↑x : Y)
x : Y
⊢ x ∈ C ↔ ∃ (a : Y) (h : a ∈ C), f (g (Subtype.mk (p := fun (a : Y) ↦ a ∈ C) a ⋯)) = x

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
refine_2 :
  ∀ (C' : Set X) (hC'_subset : C' ⊆ A) (hC_subset : f '' C' ⊆ f '' A) (hC_cover : IsCover ε (f '' A) (f '' C')),
    ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ (f '' C').encard
⊢ ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ C.encard

Tactic:
obtain ⟨C', hC'_subset, rfl⟩ : ∃ C', C' ⊆ A ∧ C = C'.image f := by
      have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
      choose g hg_mem hg using this
      refine ⟨Set.range g, ?_, ?_⟩
      · rwa [Set.range_subset_iff]
      · ext
        simp
        grind

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε (f '' A) (f '' C')
⊢ ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ (f '' C').encard

Tactic:
(iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
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
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε (f '' A) (f '' C')
refine_2 : ⨅ (_ : IsCover ε A C'), C'.encard ≤ (f '' C').encard
⊢ ⨅ (C : Set X), ⨅ (_ : C ⊆ A), ⨅ (_ : IsCover ε A C), C.encard ≤ (f '' C').encard

Tactic:
refine (iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_

Premises used: LE.le.trans, iInf_le