awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
s : Set α
hy : y ∈ s
i : α
hi : i ∈ s
⊢ edist x y ≤ edist x i + ediam s

Tactic:
calc
    edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
    _ ≤ edist x i + Metric.ediam s := add_le_add le_rfl (Metric.edist_le_ediam_of_mem hi hy)

Premises used: le_rfl, add_le_add, Metric.edist_le_ediam_of_mem, Metric.ediam, EDist.edist, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ ∀ (x y : α), infEDist x s ≤ infEDist y s + 1 * edist x y

Tactic:
simp only [one_mul, infEDist_le_infEDist_add_edist, forall₂_true_iff]

Premises used: Metric.infEDist_le_infEDist_add_edist, forall₂_true_iff, one_mul
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s

Tactic:
le_antisymm (infEDist_anti subset_closure) ?_

Premises used: subset_closure, Metric.infEDist_anti, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
refine : infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s

Tactic:
refine le_antisymm (infEDist_anti subset_closure) ?_

Premises used: subset_closure, Metric.infEDist_anti, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
refine :
  ∀ (ε : ℝ≥0) (εpos : 0 < ε) (h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞),
    infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ 0 < (↑ε : ℝ≥0∞) / 2

Tactic:
simpa [pos_iff_ne_zero] using εpos

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
⊢ 0 < (↑ε : ℝ≥0∞) / 2

Tactic:
have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2

Tactic:
have : infEDist x (closure s) < infEDist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
obtain :
  ∀ (y : α) (ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
    (hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2),
    infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEDist x (closure s) + ↑ε / 2⟩ :=
    infEDist_lt_iff.mp this

Premises used: Metric.infEDist, closure, Iff.mp, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
obtain :
  ∀ (z : α) (zs : z ∈ s) (dyz : edist y z < (↑ε : ℝ≥0∞) / 2),
    infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ infEDist x s ≤ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0

Premises used: ENNReal.ofNNReal, HDiv.hDiv, Iff.mp, EMetric.mem_closure_iff, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
⊢ infEDist x s ≤ edist x z

Tactic:
infEDist_le_edist_of_mem zs

Premises used: Metric.infEDist_le_edist_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
⊢ edist x z ≤ edist x y + edist y z

Tactic:
edist_triangle _ _ _

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
⊢ edist x y + edist y z ≤
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2

Tactic:
add_le_add (le_of_lt hy) (le_of_lt dyz)

Premises used: add_le_add, le_of_lt
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
rw :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + ((↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2) =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
rw₁ rw₂ :
  infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 + (↑ε : ℝ≥0∞) / 2 =
    infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)

Tactic:
rw [add_assoc, ENNReal.add_halves]

Premises used: add_assoc, ENNReal.add_halves
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
ε : ℝ≥0
εpos : 0 < ε
h : Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) < ∞
ε0 : 0 < (↑ε : ℝ≥0∞) / 2
this :
  Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) <
    Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
y : α
ycs : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
hy : edist x y < Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2
z : α
zs : z ∈ s
dyz : edist y z < (↑ε : ℝ≥0∞) / 2
infEDist :
  Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞) / 2 +
      (↑ε : ℝ≥0∞) / 2 =
    Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)
⊢ Metric.infEDist x s ≤
    Metric.infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) + (↑ε : ℝ≥0∞)

Tactic:
calc
    infEDist x s ≤ edist x z := infEDist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEDist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEDist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

Premises used: Metric.infEDist_le_edist_of_mem, add_le_add, le_of_lt, Metric.infEDist, closure, EDist.edist, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0
⊢ infEDist x s = 0

Tactic:
rw [← infEDist_closure]

Premises used: Metric.infEDist_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
infEDist_zero_of_mem h

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
exact infEDist_zero_of_mem h

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : infEDist x s = 0
ε : ℝ≥0∞
εpos : ε > 0
rwa rwa₁ rwa₂ rwa₃ : 0 < ε
⊢ infEDist x s < ε

Tactic:
rwa [h]
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : x ∈ s ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
rw₁ rw₂ : x ∈ s ↔ x ∈ s
⊢ x ∈ s ↔ infEDist x s = 0

Tactic:
rw [← mem_closure_iff_infEDist_zero, h.closure_eq]

Premises used: IsClosed.closure_eq, Metric.mem_closure_iff_infEDist_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
rw : 0 < infEDist x E ↔ ¬infEDist x E = 0
rw₁ rw₂ : infEDist x E ≠ 0 ↔ ¬infEDist x E = 0
⊢ 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
rw [mem_closure_iff_infEDist_zero, pos_iff_ne_zero]

Premises used: Metric.mem_closure_iff_infEDist_zero, pos_iff_ne_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
rw : 0 < infEDist x E ↔ x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
rw₁ rw₂ :
  x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ 0 < infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) ↔
    x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
rw [infEDist_closure, infEDist_pos_iff_notMem_closure]

Premises used: Metric.infEDist_closure, Metric.infEDist_pos_iff_notMem_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∃ (r : ℝ), 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEDist x E

Tactic:
rw [← infEDist_pos_iff_notMem_closure, ENNReal.lt_iff_exists_real_btwn] at h

Premises used: ENNReal.lt_iff_exists_real_btwn, Metric.infEDist_pos_iff_notMem_closure
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
h : ∃ (r : ℝ), 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEDist x E
rcases :
  ∀ (ε : ℝ),
    0 ≤ ε →
      ∀ (ε_pos : 0 < ENNReal.ofReal ε) (ε_lt : ENNReal.ofReal ε < infEDist x E),
        ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E
⊢ ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E

Tactic:
rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
ε : ℝ
left : 0 ≤ ε
ε_pos : 0 < ENNReal.ofReal ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E

Tactic:
⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩

Premises used: ENNReal.ofReal_pos, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
E : Set α
ε : ℝ
left : 0 ≤ ε
ε_pos : 0 < ENNReal.ofReal ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∃ (ε : ℝ), 0 < ε ∧ ENNReal.ofReal ε < infEDist x E

Tactic:
exact ⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
rw : ∀ ⦃a : α⦄, a ∈ closedEBall x r → a ∉ s
⊢ Disjoint (closedEBall x r) s

Tactic:
rw [disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
apply : infEDist x s < infEDist x s
⊢ False

Tactic:
apply lt_irrefl (infEDist x s)

Premises used: lt_irrefl, Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ infEDist x s ≤ edist x y

Tactic:
infEDist_le_edist_of_mem h'y

Premises used: Metric.infEDist_le_edist_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
rwa : ∀ (hy : edist y x ≤ r) (h'y : y ∈ s), edist x y ≤ r
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hy : edist x y ≤ r) (h'y : y ∈ s), edist x y ≤ r
⊢ edist x y ≤ r

Tactic:
rwa [Metric.mem_closedEBall, edist_comm] at hy

Premises used: PseudoEMetricSpace.edist_comm, Metric.mem_closedEBall
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
⊢ r < infEDist x s

Tactic:
h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
h : r < Metric.infEDist x s
y : α
hy : y ∈ closedEBall x r
h'y : y ∈ s
infEDist : edist x y ≤ r
⊢ Metric.infEDist x s < Metric.infEDist x s

Tactic:
calc
    infEDist x s ≤ edist x y := infEDist_le_edist_of_mem h'y
    _ ≤ r := by rwa [Metric.mem_closedEBall, edist_comm] at hy
    _ < infEDist x s := h

Premises used: Metric.infEDist_le_edist_of_mem, Metric.infEDist, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α
t : Set α
Φ : α → β
hΦ : Isometry Φ
⊢ infEDist (Φ x) (Φ '' t) = infEDist x t

Tactic:
simp only [infEDist, iInf_image, hΦ.edist_eq]

Premises used: Isometry.edist_eq, Metric.infEDist, iInf_image
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
M : Type u_2
inst_1 : SMul M α
inst_2 : IsIsometricSMul M α
c : M
x : α
s : Set α
⊢ infEDist (c • x) (c • s) = infEDist x s

Tactic:
infEDist_image (isometry_smul _ _)

Premises used: Metric.infEDist_image, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ∃ (a : ℝ≥0∞), 0 < a ∧ a < 1

Tactic:
exists_between zero_lt_one

Premises used: exists_between, zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
obtain :
  ∀ (a : ℝ≥0∞) (a_pos : 0 < a) (a_lt_one : a < 1),
    ∃ (F : ℕ → Set α),
      (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
        (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F

Tactic:
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one

Premises used: exists_between, zero_lt_one
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
by_contra : ∀ (h : x ∉ U), False
⊢ x ∈ U

Tactic:
by_contra h
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : x ∉ U
⊢ infEDist x Uᶜ ≠ 0

Tactic:
have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : x ∉ U
this : infEDist x Uᶜ ≠ 0
⊢ False

Tactic:
this (infEDist_zero_of_mem h)

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
n : ℕ
x : α
hx : x ∈ F n
h : x ∉ U
this : infEDist x Uᶜ ≠ 0
⊢ False

Tactic:
exact this (infEDist_zero_of_mem h)

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
⊢ ∀ (n : ℕ), F n ⊆ U

Tactic:
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
    by_contra h
    have : infEDist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
    exact this (infEDist_zero_of_mem h)
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F

Tactic:
⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Metric.continuous_infEDist, IsClosed.preimage, isClosed_Ici
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
refine_1 : ⋃ (n : ℕ), F n = U
refine_2 : Monotone F
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F

Tactic:
refine ⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ (n : ℕ), F n ⊆ U

Tactic:
simp only [iUnion_subset_iff, F_subset, forall_const]

Premises used: Set.iUnion_subset_iff, forall_const
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : (n : ℕ) → Set α := fun (n : ℕ) ↦ (fun (x : α) ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
refine_1 : ∀ (x : α) (hx : x ∈ U), Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
⊢ ⋃ (n : ℕ), F n = U

Tactic:
refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_

Premises used: Set.Subset.antisymm