awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have refine_1 : ⋃ (n : ℕ), F n = U
Tactic: refine ⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ ∃ (F : ℕ → Set α),
    (∀ (n : ℕ), IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (F n)) ∧
      (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ (n : ℕ), F n = U ∧ Monotone F
have refine_2 : Monotone F
Tactic: refine ⟨F, fun n => IsClosed.preimage continuous_infEDist isClosed_Ici, F_subset, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have refine_1 : ∀ (x : α) (hx : x ∈ U), Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
Tactic: refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have this : x ∉ Uᶜ
Tactic: have : x ∉ Uᶜ := by simpa using hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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ᶜ
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have this₁ : ¬infEDist x Uᶜ = 0
Tactic: rw [mem_iff_infEDist_zero_of_closed hU.isClosed_compl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have B : 0 < infEDist x Uᶜ
Tactic: have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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ᶜ
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have this₁ : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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)
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have refine_1 : ∀ (n : ℕ) (hn : a ^ n < infEDist x Uᶜ), Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
Tactic: rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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ᶜ
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), F n) x
have refine_1 : ∃ (i : ℕ), x ∈ F i
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ x ∈ F n
have refine_2 : ∀ (hx : a ^ m ≤ infEDist x Uᶜ), a ^ n ≤ infEDist x Uᶜ
Tactic: simp only [F, mem_Ici, mem_preimage] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
hs : IsCompact s
hne : s.Nonempty
x : α
⊢ ∃ y ∈ s, infEDist x s = edist x y
have A : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ edist x y
Tactic: have A : Continuous fun y => edist x y := by fun_prop
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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 ∈ s, infEDist x s = edist x y
have obtain : ∀ (y : α) (ys : y ∈ s) (hy : IsMinOn (β := ℝ≥0∞) (fun (y : α) ↦ edist x y) s y), ∃ y ∈ s, infEDist x s = edist x y
Tactic: obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ edist x y ≤ infEDist x s
have rwa : ∀ y_1 ∈ s, edist x y ≤ edist x y_1
Tactic: rwa [le_infEDist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have inl : ∀ (hs : IsCompact.{u} (X := α) ∅) (hst : Disjoint ∅ t),
  ∃ (r : ℝ≥0), 0 < r ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
Cleared hypotheses: s, hs, hst
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have inr : ∀ (hne : s.Nonempty), ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
t : Set α
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hs : IsCompact.{u} (X := α) ∅
hst : Disjoint ∅ t
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have h : LT.lt (α := ℝ≥0) 0 1 ∧ ∀ (x : α), Membership.mem (γ := Set α) ∅ x → ∀ y ∈ t, (↑1 : ℝ≥0∞) < edist x y
Tactic: use 1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : Disjoint s t
hne : s.Nonempty
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have 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
Tactic: obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEDist.continuousOn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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
⊢ ∃ (r : ℝ≥0), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have this : 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⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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), 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
have 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
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α × β
s : Set α
t : Set β
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have simp_rw : Eq (α := ℝ≥0∞) (⨅ y ∈ s ×ˢ t, edist x y) (max (⨅ y ∈ s, edist x.1 y) (⨅ y ∈ t, edist x.2 y))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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))
⊢ infEDist x (s ×ˢ t) = max (infEDist x.1 s) (infEDist x.2 t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s s = 0
have simp : ∀ (i : α) (i_1 : i ∈ s), infEDist i s = 0
Tactic: simp only [hausdorffEDist_def, sup_idem, ENNReal.iSup_eq_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEDist s t = hausdorffEDist t s
have 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))
Tactic: simp only [hausdorffEDist_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, infEDist x t ≤ r
H2 : ∀ x ∈ t, infEDist x s ≤ r
⊢ hausdorffEDist s t ≤ r
have simp : (∀ (i : α) (i_1 : i ∈ s), infEDist i t ≤ r) ∧ ∀ (i : α) (i_1 : i ∈ t), infEDist i s ≤ r
Tactic: simp only [hausdorffEDist_def, sup_le_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
have refine_1 : ∀ (x : α) (xs : x ∈ s), infEDist x t ≤ r
Tactic: refine hausdorffEDist_le_of_infEDist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ hausdorffEDist s t ≤ r
have refine_2 : ∀ (x : α) (xt : x ∈ t), infEDist x s ≤ r
Tactic: refine hausdorffEDist_le_of_infEDist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infEDist x t ≤ r
have refine_1 : ∀ (y : α) (yt : y ∈ t) (hy : edist x y ≤ r), infEDist x t ≤ r
Tactic: rcases H1 x xs with ⟨y, yt, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infEDist x s ≤ r
have refine_2 : ∀ (y : α) (ys : y ∈ s) (hy : edist x y ≤ r), infEDist x s ≤ r
Tactic: rcases H2 x xt with ⟨y, ys, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEDist x t ≤ hausdorffEDist s t
have rw : infEDist x t ≤ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s)
Tactic: rw [hausdorffEDist_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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)
have refine : infEDist x t ≤ ⨆ x ∈ s, infEDist x t
Tactic: refine le_trans ?_ le_sup_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEDist x s + hausdorffEDist s t < ∞
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have ε0 : (↑ε : ℝ≥0∞) / 2 ≠ 0
Tactic: have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (hypothesis)
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 t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.HausdorffDistance (goal)
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
⊢ infEDist x t ≤ infEDist x s + hausdorffEDist s t + (↑ε : ℝ≥0∞)
have obtain : ∀ (y : α) (ys : y ∈ s) (dxy : edist x y < infEDist x s + (↑ε : ℝ≥0∞) / 2),
  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