awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
hu' : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
Filter.extraction_forall_of_eventually hu'

Premises used: Filter.extraction_forall_of_eventually
-- Module: Mathlib.Topology.MetricSpace.Cauchy
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ (N : ℕ), ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
hu' : ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k
⊢ ∃ (f : ℕ → ℕ), StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
exact Filter.extraction_forall_of_eventually hu'

Premises used: Filter.extraction_forall_of_eventually
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : hausdorffEDist s t < δ
⊢ ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ

Tactic:
rw [hausdorffEDist, max_lt_iff] at h

Premises used: max_lt_iff, Metric.hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
h₁ : ∀ (x : α × α), edist x.1 x.2 < δ
| (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 < δ} (s, t).1

Tactic:
enter [2, 2, 1, 1, _]
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
x : α × α
h₁ : edist x.2 x.1 < δ
| edist x.1 x.2 < δ

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
h₁ : ∀ (x : α × α), edist x.2 x.1 < δ
| (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 < δ} (s, t).1

Tactic:
enter [2, 2, 1, 1, _]; rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
conv :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 < δ} (s, t).1
⊢ (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 < δ} (s, t).1

Tactic:
conv => enter [2, 2, 1, 1, _]; rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s_1 t_1 : Set α
δ : ℝ≥0∞
h_1 : ⨆ x ∈ s_1, infEDist x t_1 < δ ∧ ⨆ y ∈ t_1, infEDist y s_1 < δ
s t : Set α
h : ⨆ x ∈ s, infEDist x t < δ
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α) (SetRel.preimage {p : α × α | edist p.1 p.2 < δ} t) x

Tactic:
simpa only [infEDist, iInf_lt_iff, exists_prop] using (le_iSup₂ x hx).trans_lt h

Premises used: le_iSup₂, Metric.infEDist, exists_prop, iInf_lt_iff, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
⊢ ∀ {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ), s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} t

Tactic:
have {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ) :
      s ⊆ SetRel.preimage {p | edist p.1 p.2 < δ} t := by
    intro x hx
    simpa only [infEDist, iInf_lt_iff, exists_prop] using (le_iSup₂ x hx).trans_lt h
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
this : ∀ {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ), s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} t
⊢ (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 < δ} (s, t).1

Tactic:
⟨this h.1, this h.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
this : ∀ {s t : Set α} (h : ⨆ x ∈ s, infEDist x t < δ), s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} t
⊢ (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 < δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 < δ} (s, t).1

Tactic:
exact ⟨this h.1, this h.2⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : Membership.mem (γ := SetRel (Set α) (Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) (s, t)
rw : ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
⊢ hausdorffEDist s t ≤ δ

Tactic:
rw [hausdorffEDist, max_le_iff]

Premises used: max_le_iff, Metric.hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : Membership.mem (γ := SetRel (Set α) (Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) (s, t)
⊢ (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1

Tactic:
rw [hausdorffEntourage, Set.mem_setOf] at h

Premises used: Set.mem_setOf, hausdorffEntourage
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
h₁ : ∀ (x : α × α), edist x.1 x.2 ≤ δ
| (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1

Tactic:
enter [2, 2, 1, 1, _]
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
x : α × α
h₁ : edist x.2 x.1 ≤ δ
| edist x.1 x.2 ≤ δ

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
h₁ : ∀ (x : α × α), edist x.2 x.1 ≤ δ
| (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1

Tactic:
enter [2, 2, 1, 1, _]; rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
⊢ (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s, t).1

Tactic:
conv at h => enter [2, 2, 1, 1, _]; rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s_1 t_1 : Set α
δ : ℝ≥0∞
h_1 :
  (s_1, t_1).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s_1, t_1).2 ∧
    (s_1, t_1).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s_1, t_1).1
s t : Set α
h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t
rw : ∀ (i : α) (j : i ∈ s), infEDist i t ≤ δ
⊢ ⨆ x ∈ s, infEDist x t ≤ δ

Tactic:
rw [iSup₂_le_iff]

Premises used: iSup₂_le_iff
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s_1 t_1 : Set α
δ : ℝ≥0∞
h_1 :
  (s_1, t_1).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s_1, t_1).2 ∧
    (s_1, t_1).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s_1, t_1).1
s t : Set α
h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t
x : α
hx : x ∈ s
obtain :
  ∀ (y : α) (hy : y ∈ t) (hxy : Membership.mem (γ := SetRel α α) {p : α × α | edist p.1 p.2 ≤ δ} (x, y)),
    infEDist x t ≤ δ
⊢ infEDist x t ≤ δ

Tactic:
obtain ⟨y, hy, hxy⟩ := h hx
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s_1 t_1 : Set α
δ : ℝ≥0∞
h_1 :
  (s_1, t_1).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s_1, t_1).2 ∧
    (s_1, t_1).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s_1, t_1).1
s t : Set α
h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Membership.mem (γ := SetRel α α) {p : α × α | edist p.1 p.2 ≤ δ} (x, y)
⊢ infEDist x t ≤ δ

Tactic:
iInf₂_le_of_le y hy hxy

Premises used: iInf₂_le_of_le, Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s_1 t_1 : Set α
δ : ℝ≥0∞
h_1 :
  (s_1, t_1).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s_1, t_1).2 ∧
    (s_1, t_1).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s_1, t_1).1
s t : Set α
h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t
x : α
hx : x ∈ s
y : α
hy : y ∈ t
hxy : Membership.mem (γ := SetRel α α) {p : α × α | edist p.1 p.2 ≤ δ} (x, y)
⊢ infEDist x t ≤ δ

Tactic:
exact iInf₂_le_of_le y hy hxy

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s, t).1
⊢ ∀ {s t : Set α} (h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t), ⨆ x ∈ s, infEDist x t ≤ δ

Tactic:
have {s t : Set α} (h : s ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} t) :
      ⨆ x ∈ s, infEDist x t ≤ δ := by
    rw [iSup₂_le_iff]
    intro x hx
    obtain ⟨y, hy, hxy⟩ := h hx
    exact iInf₂_le_of_le y hy hxy
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s, t).1
this : ∀ {s t : Set α} (h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t), ⨆ x ∈ s, infEDist x t ≤ δ
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
⟨this h.1, this h.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} (s, t).2 ∧
    (s, t).2 ⊆ SetRel.image {x : α × α | edist x.2 x.1 ≤ δ} (s, t).1
this : ∀ {s t : Set α} (h : s ⊆ SetRel.preimage {p : α × α | edist p.1 p.2 ≤ δ} t), ⨆ x ∈ s, infEDist x t ≤ δ
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
exact ⟨this h.1, this h.2⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Eq.{u_1 + 1} (α := Filter (Set α × Set α)) (uniformity (Set α))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε})

Tactic:
le_antisymm
      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
        mem_hausdorffEntourage_of_hausdorffEDist_lt)

Premises used: Iff.mpr, monotone_hausdorffEntourage, uniformity_basis_edist, Filter.le_principal_iff, Filter.HasBasis.ge_iff, Filter.mem_iInf_of_mem, le_iInf₂, le_antisymm, Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt, Filter.HasBasis.lift'
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
refine :
  ∀ (ε : ℝ≥0∞) (hε : ε > 0),
    Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
⊢ Eq.{u_1 + 1} (α := Filter (Set α × Set α)) (uniformity (Set α))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε})

Tactic:
refine le_antisymm
      (le_iInf₂ fun ε hε => Filter.le_principal_iff.mpr ?_)
      (uniformity_basis_edist.lift' monotone_hausdorffEntourage |>.ge_iff.mpr fun ε hε =>
        Filter.mem_iInf_of_mem ε <| Filter.mem_iInf_of_mem hε fun _ =>
        mem_hausdorffEntourage_of_hausdorffEDist_lt)

Premises used: Iff.mpr, monotone_hausdorffEntourage, uniformity_basis_edist, Filter.le_principal_iff, Filter.HasBasis.ge_iff, Filter.mem_iInf_of_mem, le_iInf₂, le_antisymm, Metric.mem_hausdorffEntourage_of_hausdorffEDist_lt, Filter.HasBasis.lift'
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
obtain :
  ∀ (δ : ℝ≥0∞) (hδ : 0 < δ) (hδε : δ < ε),
    Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
⊢ Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}

Tactic:
obtain ⟨δ, hδ, hδε⟩ := exists_between hε

Premises used: exists_between
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
δ : ℝ≥0∞
hδ : 0 < δ
hδε : δ < ε
a : Set α × Set α
h : Membership.mem (γ := Set (Set α × Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) a
⊢ hausdorffEDist a.1 a.2 < ε

Tactic:
hδε.trans_le' <| hausdorffEDist_le_of_mem_hausdorffEntourage h

Premises used: Metric.hausdorffEDist_le_of_mem_hausdorffEntourage, LT.lt.trans_le'
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
δ : ℝ≥0∞
hδ : 0 < δ
hδε : δ < ε
h :
  ∀ (a : Set α × Set α),
    Membership.mem (γ := Set (Set α × Set α))
      {x : Set α × Set α |
        Membership.mem (γ := Set (Set α × Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) x →
          Membership.mem (γ := Set (Set α × Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε} x}
      a
h₁ h₂ :
  ∀ (a : Set α × Set α)
    (h : Membership.mem (γ := Set (Set α × Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) a),
    hausdorffEDist a.1 a.2 < ε
⊢ Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}

Tactic:
filter_upwards [Filter.mem_lift' (uniformity_basis_edist_le.mem_of_mem hδ)]
      with _ h using hδε.trans_le' <| hausdorffEDist_le_of_mem_hausdorffEntourage h

Premises used: uniformity_basis_edist_le, Filter.mem_lift', LT.lt.trans_le', Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
refine : ∀ (x y : α × Closeds α), infEDist x.1 (↑x.2 : Set α) ≤ infEDist y.1 (↑y.2 : Set α) + 2 * edist x y
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × Closeds α) ↦ infEDist p.1 (↑p.2 : Set α)

Tactic:
refine continuous_of_le_add_edist 2 (by simp) ?_

Premises used: continuous_of_le_add_edist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x (↑s : Set α) ≤ infEDist x (↑t : Set α) + hausdorffEDist (↑t : Set α) (↑s : Set α)

Tactic:
infEDist_le_infEDist_add_hausdorffEDist

Premises used: Metric.infEDist_le_infEDist_add_hausdorffEDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
bc : infEDist x (↑t : Set α) ≤ infEDist y (↑t : Set α) + edist x y
⊢ infEDist x (↑t : Set α) + hausdorffEDist (↑t : Set α) (↑s : Set α) ≤
    infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x (↑t : Set α) ≤ infEDist y (↑t : Set α) + edist x y

Tactic:
apply infEDist_le_infEDist_add_edist

Premises used: Metric.infEDist_le_infEDist_add_edist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
rw :
  infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α)) =
    infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))
rw₁ rw₂ :
  infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α)) =
    infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))
⊢ infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α) =
    infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))

Tactic:
rw [add_assoc, hausdorffEDist_comm]

Premises used: add_assoc, Metric.hausdorffEDist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
bc : edist x y ≤ edist (x, s) (y, t)
bc₁ : hausdorffEDist (↑s : Set α) (↑t : Set α) ≤ edist (x, s) (y, t)
⊢ infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α)) ≤
    infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t))

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ edist x y ≤ edist (x, s) (y, t)

Tactic:
apply_rules [le_max_left, le_max_right]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ hausdorffEDist (↑s : Set α) (↑t : Set α) ≤ edist (x, s) (y, t)

Tactic:
apply_rules [le_max_left, le_max_right]

Premises used: le_max_right, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
rw : infEDist y (↑t : Set α) + edist (x, s) (y, t) * 2 = infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
rw₁ rw₂ : infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t) = infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
⊢ infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t)) =
    infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)

Tactic:
rw [← mul_two, mul_comm]

Premises used: mul_comm, mul_two
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
infEDist :
  Metric.infEDist x (↑t : Set α) + hausdorffEDist (↑t : Set α) (↑s : Set α) ≤
    Metric.infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α)
infEDist₁ :
  Metric.infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α) =
    Metric.infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))
infEDist₂ :
  Metric.infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α)) ≤
    Metric.infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t))
infEDist₃ :
  Metric.infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t)) =
    Metric.infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
⊢ Metric.infEDist (x, s).1 (↑(x, s).2 : Set α) ≤ Metric.infEDist (y, t).1 (↑(y, t).2 : Set α) + 2 * edist (x, s) (y, t)

Tactic:
calc
    infEDist x s ≤ infEDist x t + hausdorffEDist (t : Set α) s :=
      infEDist_le_infEDist_add_hausdorffEDist
    _ ≤ infEDist y t + edist x y + hausdorffEDist (t : Set α) s := by
      gcongr; apply infEDist_le_infEDist_add_edist
    _ = infEDist y t + (edist x y + hausdorffEDist (s : Set α) t) := by
      rw [add_assoc, hausdorffEDist_comm]
    _ ≤ infEDist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = infEDist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]

Premises used: Prod.mk, Metric.infEDist, SetLike.coe, HAdd.hAdd, Metric.hausdorffEDist, Metric.infEDist_le_infEDist_add_hausdorffEDist, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
s t : Closeds α
⊢ edist s t = hausdorffEDist (↑s : Set α) (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ ∀ (n : ℕ), 0 < B n

Tactic:
simp [B, ENNReal.pow_pos]

Premises used: ENNReal.pow_pos
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
⊢ ∀ (n : ℕ), 0 < B n

Tactic:
have B_pos : ∀ n, (0 : ℝ≥0∞) < B n := by simp [B, ENNReal.pow_pos]
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
⊢ ∀ (n : ℕ), B n ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
⊢ ∀ (n : ℕ), B n ≠ ∞

Tactic:
have B_ne_top : ∀ n, B n ≠ ⊤ := by finiteness
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
⊢ CompleteSpace.{u_1} (Closeds α)

Tactic:
EMetric.complete_of_convergent_controlled_sequences B B_pos fun s hs => ?_

Premises used: EMetric.complete_of_convergent_controlled_sequences
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
refine :
  ∀ (s : ℕ → Closeds α) (hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N),
    ∃ (x : Closeds α), Tendsto s atTop (𝓝 x)
⊢ CompleteSpace.{u_1} (Closeds α)

Tactic:
refine EMetric.complete_of_convergent_controlled_sequences B B_pos fun s hs => ?_

Premises used: EMetric.complete_of_convergent_controlled_sequences
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
h : Tendsto s atTop (𝓝 t)
⊢ ∃ (x : Closeds α), Tendsto s atTop (𝓝 x)

Tactic:
use t
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ ∃ z' ∈ s (n + l + 1), edist (↑z : α) z' < B n / HPow.hPow (α := ℝ≥0∞) 2 l

Tactic:
exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_

Premises used: Metric.exists_edist_lt_of_hausdorffEDist_lt