awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : α
hx : x ∈ U
⊢ x ∉ Uᶜ

Tactic:
simpa using hx
-- 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
x : α
hx : x ∈ U
⊢ x ∉ Uᶜ

Tactic:
have : x ∉ Uᶜ := by simpa using hx
-- 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
x : α
hx : x ∈ U
this : x ∉ Uᶜ
⊢ ¬infEDist x Uᶜ = 0

Tactic:
rw [mem_iff_infEDist_zero_of_closed hU.isClosed_compl] at this

Premises used: IsOpen.isClosed_compl, Metric.mem_iff_infEDist_zero_of_closed
-- 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
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
⊢ 0 < infEDist x Uᶜ

Tactic:
simpa [pos_iff_ne_zero] using this

Premises used: pos_iff_ne_zero
-- 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
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
⊢ 0 < infEDist x Uᶜ

Tactic:
have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this
-- 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
x : α
hx : x ∈ U
this : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ a ^ n) atTop (𝓝 0)

Tactic:
have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
      ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_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)
F_subset : ∀ (n : ℕ), F n ⊆ U
x : α
hx : x ∈ U
this_1 : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ a ^ n) atTop (𝓝 0)
refine_1 : ∀ (n : ℕ) (hn : a ^ n < infEDist x Uᶜ), Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x

Tactic:
rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- 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
x : α
hx : x ∈ U
this_1 : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEDist x Uᶜ
refine_1 : ∃ (i : ℕ), x ∈ F i
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- 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
x : α
hx : x ∈ U
this_1 : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEDist x Uᶜ
⊢ ∃ (i : ℕ), x ∈ F i

Tactic:
⟨n, hn.le⟩

Premises used: LT.lt.le, Exists.intro
-- 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
x : α
hx : x ∈ U
this_1 : ¬infEDist x Uᶜ = 0
B : 0 < infEDist x Uᶜ
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ a ^ n) atTop (𝓝 0)
n : ℕ
hn : a ^ n < infEDist x Uᶜ
⊢ ∃ (i : ℕ), x ∈ F i

Tactic:
exact ⟨n, hn.le⟩
-- 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
m n : ℕ
hmn : m ≤ n
x : α
hx : x ∈ F m
refine_2 : ∀ (hx : a ^ m ≤ infEDist x Uᶜ), a ^ n ≤ infEDist x Uᶜ
⊢ x ∈ F n

Tactic:
simp only [F, mem_Ici, mem_preimage] at hx ⊢

Premises used: Set.mem_Ici, Set.mem_preimage
-- 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
m n : ℕ
hmn : m ≤ n
x : α
hx : a ^ m ≤ infEDist x Uᶜ
⊢ a ^ n ≤ infEDist x Uᶜ

Tactic:
apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx

Premises used: LT.lt.le, pow_le_pow_right_of_le_one', le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y

Tactic:
have A : Continuous fun y => edist x y := by fun_prop
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y
obtain :
  ∀ (y : α) (ys : y ∈ s) (hy : IsMinOn (β := ℝ≥0∞) (fun (y : α) ↦ edist x y) s y), ∃ y ∈ s, infEDist x s = edist x y
⊢ ∃ y ∈ s, infEDist x s = edist x y

Tactic:
obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn

Premises used: Continuous.continuousOn, IsCompact.exists_isMinOn
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (β := ℝ≥0∞) (fun (y : α) ↦ edist x y) s y
rwa rwa₁ rwa₂ rwa₃ : ∀ y_1 ∈ s, edist x y ≤ edist x y_1
⊢ edist x y ≤ infEDist x s

Tactic:
rwa [le_infEDist]

Premises used: Metric.le_infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y
y : α
ys : y ∈ s
hy : IsMinOn (β := ℝ≥0∞) (fun (y : α) ↦ edist x y) s y
⊢ ∃ y ∈ s, infEDist x s = edist x y

Tactic:
exact ⟨y, ys, le_antisymm (infEDist_le_edist_of_mem ys) (by rwa [le_infEDist])⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
inl :
  ∀ (hs : IsCompact.{u} (X := α) ∅) (hst : Disjoint ∅ t),
    ∃ (r : ℝ≥0), 0 < r ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
inr : ∀ (hne : s.Nonempty), ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hs : IsCompact.{u} (X := α) ∅
hst : Disjoint ∅ t
h : LT.lt (α := ℝ≥0) 0 1 ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑1 : ℝ≥0∞) < edist x y
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
use 1
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hs : IsCompact.{u} (X := α) ∅
hst : Disjoint ∅ t
⊢ LT.lt (α := ℝ≥0) 0 1 ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑1 : ℝ≥0∞) < edist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
inr :
  ∀ (x : α) (hx : x ∈ s) (h : IsMinOn (β := ℝ≥0∞) (fun (x : α) ↦ infEDist x t) s x),
    ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEDist.continuousOn

Premises used: Continuous.continuousOn, IsCompact.exists_isMinOn, Metric.continuous_infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (β := ℝ≥0∞) (fun (x : α) ↦ infEDist x t) s x
⊢ 0 < infEDist x t

Tactic:
have : 0 < infEDist x t :=
    pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEDist_zero_of_closed ht).mpr H⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (β := ℝ≥0∞) (fun (x : α) ↦ infEDist x t) s x
this : 0 < infEDist x t
inr :
  ∀ (r : ℝ≥0) (h₀ : 0 < (↑r : ℝ≥0∞)) (hr : (↑r : ℝ≥0∞) < infEDist x t),
    ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (β := ℝ≥0∞) (fun (x : α) ↦ infEDist x t) s x
this : 0 < infEDist x t
r : ℝ≥0
h₀ : 0 < (↑r : ℝ≥0∞)
hr : (↑r : ℝ≥0∞) < infEDist x t
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEDist.1 (h hy) z hz⟩

Premises used: Metric.le_infEDist, ENNReal.coe_pos, LT.lt.trans_le, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
x : α
hx : x ∈ s
h : IsMinOn (β := ℝ≥0∞) (fun (x : α) ↦ infEDist x t) s x
this : 0 < infEDist x t
r : ℝ≥0
h₀ : 0 < (↑r : ℝ≥0∞)
hr : (↑r : ℝ≥0∞) < infEDist x t
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y

Tactic:
exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEDist.1 (h hy) z hz⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
simp_rw : Eq (α := ℝ≥0∞) (⨅ y ∈ s ×ˢ t, edist x y) (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨅ y ∈ s ×ˢ t, max (edist x.1 y.1) (edist x.2 y.2)) (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
simp_rw₂ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : (i, j) ∈ s ×ˢ t), max (edist x.1 (i, j).1) (edist x.2 (i, j).2))
    (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
simp_rw₃ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : (i, j).1 ∈ s ∧ (i, j).2 ∈ t), max (edist x.1 i) (edist x.2 j))
    (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
simp_rw₄ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : i ∈ s), ⨅ (_ : j ∈ t), max (edist x.1 i) (edist x.2 j))
    (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
simp_rw₅ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : i ∈ s), ⨅ (_ : j ∈ t), max (edist x.1 i) (edist x.2 j))
    (⨅ (i : α), max (⨅ (_ : i ∈ s), edist x.1 i) (⨅ y ∈ t, edist x.2 y))
simp_rw₆ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : i ∈ s), ⨅ (_ : j ∈ t), max (edist x.1 i) (edist x.2 j))
    (⨅ (i : α), ⨅ (i_1 : β), max (⨅ (_ : i ∈ s), edist x.1 i) (⨅ (_ : i_1 ∈ t), edist x.2 i_1))
simp_rw₇ :
  Eq (α := ℝ≥0∞) (⨅ (i : α), ⨅ (j : β), ⨅ (_ : i ∈ s), ⨅ (_ : j ∈ t), max (edist x.1 i) (edist x.2 j))
    (⨅ (i : α), ⨅ (i_1 : β), ⨅ (_ : i ∈ s), max (edist x.1 i) (⨅ (_ : i_1 ∈ t), edist x.2 i_1))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)

Tactic:
simp_rw +singlePass [infEDist, Prod.edist_eq, iInf_prod, Set.mem_prod, iInf_and, iInf_sup_eq,
    sup_iInf_eq, iInf_sup_eq, sup_iInf_eq]

Premises used: Prod.edist_eq, Metric.infEDist, Set.mem_prod, iInf_and, iInf_sup_eq, iInf_prod, sup_iInf_eq
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
simp : ∀ (i : α) (i_1 : i ∈ s), infEDist i s = 0
⊢ hausdorffEDist s s = 0

Tactic:
simp only [hausdorffEDist_def, sup_idem, ENNReal.iSup_eq_zero]

Premises used: Metric.hausdorffEDist_def, sup_idem, ENNReal.iSup_eq_zero
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ ∀ (i : α) (i_1 : i ∈ s), infEDist i s = 0

Tactic:
fun x hx => infEDist_zero_of_mem hx

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ ∀ (i : α) (i_1 : i ∈ s), infEDist i s = 0

Tactic:
exact fun x hx => infEDist_zero_of_mem hx

Premises used: Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
simp :
  Eq (α := ℝ≥0∞) (max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s))
    (max (⨆ y ∈ t, infEDist y s) (⨆ x ∈ s, infEDist x t))
⊢ hausdorffEDist s t = hausdorffEDist t s

Tactic:
simp only [hausdorffEDist_def]

Premises used: Metric.hausdorffEDist_def
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ Eq (α := ℝ≥0∞) (max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s))
    (max (⨆ y ∈ t, infEDist y s) (⨆ x ∈ s, infEDist x t))

Tactic:
apply sup_comm

Premises used: sup_comm
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
simp : (∀ (i : α) (i_1 : i ∈ s), infEDist i t ≤ r) ∧ ∀ (i : α) (i_1 : i ∈ t), infEDist i s ≤ r
⊢ hausdorffEDist s t ≤ r

Tactic:
simp only [hausdorffEDist_def, sup_le_iff, iSup_le_iff]

Premises used: Metric.hausdorffEDist_def, sup_le_iff, iSup_le_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
⊢ (∀ (i : α) (i_1 : i ∈ s), infEDist i t ≤ r) ∧ ∀ (i : α) (i_1 : i ∈ t), infEDist i s ≤ r

Tactic:
⟨H1, H2⟩

Premises used: And.intro
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
⊢ (∀ (i : α) (i_1 : i ∈ s), infEDist i t ≤ r) ∧ ∀ (i : α) (i_1 : i ∈ t), infEDist i s ≤ r

Tactic:
exact ⟨H1, H2⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
⊢ hausdorffEDist s t ≤ r

Tactic:
hausdorffEDist_le_of_infEDist (fun x xs ↦ ?_) (fun x xt ↦ ?_)

Premises used: Metric.hausdorffEDist_le_of_infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
refine_1 : ∀ (x : α) (xs : x ∈ s), infEDist x t ≤ r
refine_2 : ∀ (x : α) (xt : x ∈ t), infEDist x s ≤ r
⊢ hausdorffEDist s t ≤ r

Tactic:
refine hausdorffEDist_le_of_infEDist (fun x xs ↦ ?_) (fun x xt ↦ ?_)

Premises used: Metric.hausdorffEDist_le_of_infEDist
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
refine_1 : ∀ (y : α) (yt : y ∈ t) (hy : edist x y ≤ r), infEDist x t ≤ r
⊢ infEDist x t ≤ r

Tactic:
rcases H1 x xs with ⟨y, yt, hy⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEDist x t ≤ r

Tactic:
le_trans (infEDist_le_edist_of_mem yt) hy

Premises used: Metric.infEDist_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEDist x t ≤ r

Tactic:
exact le_trans (infEDist_le_edist_of_mem yt) hy

Premises used: Metric.infEDist_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
refine_2 : ∀ (y : α) (ys : y ∈ s) (hy : edist x y ≤ r), infEDist x s ≤ r
⊢ infEDist x s ≤ r

Tactic:
rcases H2 x xt with ⟨y, ys, hy⟩
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEDist x s ≤ r

Tactic:
le_trans (infEDist_le_edist_of_mem ys) hy

Premises used: Metric.infEDist_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xt : x ∈ t
y : α
ys : y ∈ s
hy : edist x y ≤ r
⊢ infEDist x s ≤ r

Tactic:
exact le_trans (infEDist_le_edist_of_mem ys) hy

Premises used: Metric.infEDist_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
rw : infEDist x t ≤ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s)
⊢ infEDist x t ≤ hausdorffEDist s t

Tactic:
rw [hausdorffEDist_def]

Premises used: Metric.hausdorffEDist_def
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s)

Tactic:
le_trans ?_ le_sup_left

Premises used: le_sup_left, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
refine : infEDist x t ≤ ⨆ x ∈ s, infEDist x t
⊢ infEDist x t ≤ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s)

Tactic:
refine le_trans ?_ le_sup_left

Premises used: le_sup_left, le_trans
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ ⨆ x ∈ s, infEDist x t

Tactic:
le_iSup₂ (α := ℝ≥0∞) x h

Premises used: le_iSup₂
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ ⨆ x ∈ s, infEDist x t

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) x h

Premises used: le_iSup₂
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
r : ℝ≥0∞
h : x ∈ s
H : hausdorffEDist s t < r
⊢ ∃ y ∈ t, edist x y < r

Tactic:
infEDist_lt_iff.mp <|
    calc
      infEDist x t ≤ hausdorffEDist s t := infEDist_le_hausdorffEDist_of_mem h
      _ < r := H

Premises used: Trans.trans, Metric.infEDist_le_hausdorffEDist_of_mem, Iff.mp, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
⊢ (↑ε : ℝ≥0∞) / 2 ≠ 0

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 t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
⊢ (↑ε : ℝ≥0∞) / 2 ≠ 0

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

Tactic:
have : infEDist x s < infEDist x s + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
obtain :
  ∀ (y : α) (ys : y ∈ s) (dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2),
    infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEDist x s + ↑ε / 2⟩ := infEDist_lt_iff.mp this

Premises used: Metric.infEDist, Iff.mp, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.HausdorffDistance
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
this : infEDist x s < infEDist x s + (↑ε : ℝ≥0∞) / 2
y : α
ys : y ∈ s
dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2
⊢ hausdorffEDist s t < hausdorffEDist s t + (↑ε : ℝ≥0∞) / 2

Tactic:
have : hausdorffEDist s t < hausdorffEDist s t + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0