awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
have h₁ : ∀ (x : α × α), edist x.1 x.2 ≤ δ
Tactic: enter [2, 2, 1, 1, _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 : α × α
| edist x.1 x.2 ≤ δ
have h₁ : edist x.2 x.1 ≤ δ
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 {p : α × α | edist p.1 p.2 ≤ δ} (s, t).1
have h₁ : ∀ (x : α × α), edist x.2 x.1 ≤ δ
Tactic: enter [2, 2, 1, 1, _]; rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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 ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
have 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
Tactic: conv at h => enter [2, 2, 1, 1, _]; rw [edist_comm]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 ∈ s, infEDist x t ≤ δ
have rw : ∀ (i : α) (j : i ∈ s), infEDist i t ≤ δ
Tactic: rw [iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ infEDist x t ≤ δ
have obtain : ∀ (y : α) (hy : y ∈ t) (hxy : Membership.mem (γ := SetRel α α) {p : α × α | edist p.1 p.2 ≤ δ} (x, y)), infEDist x t ≤ δ
Tactic: obtain ⟨y, hy, hxy⟩ := h hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
have this : ∀ {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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 < ε})
have refine : ∀ (ε : ℝ≥0∞) (hε : ε > 0),
  Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
⊢ Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
have obtain : ∀ (δ : ℝ≥0∞) (hδ : 0 < δ) (hδε : δ < ε),
  Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
Tactic: obtain ⟨δ, hδ, hδε⟩ := exists_between hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
hε : ε > 0
δ : ℝ≥0∞
hδ : 0 < δ
hδε : δ < ε
⊢ Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
have 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
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ Membership.mem (γ := Filter (Set α × Set α)) (uniformity (Set α)) {p : Set α × Set α | hausdorffEDist p.1 p.2 < ε}
have h₁ : ∀ (a : Set α × Set α),
  Membership.mem (γ := Set (Set α × Set α)) (hausdorffEntourage {p : α × α | edist p.1 p.2 ≤ δ}) a →
    hausdorffEDist a.1 a.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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × Closeds α) ↦ infEDist p.1 (↑p.2 : Set α)
have refine : ∀ (x y : α × Closeds α), infEDist x.1 (↑x.2 : Set α) ≤ infEDist y.1 (↑y.2 : Set α) + 2 * edist x y
Tactic: refine continuous_of_le_add_edist 2 (by simp) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist x (↑t : Set α) + hausdorffEDist (↑t : Set α) (↑s : Set α) ≤
    infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α)
have bc : infEDist x (↑t : Set α) ≤ infEDist y (↑t : Set α) + edist x y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α) =
    infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))
have 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 α))
Tactic: rw [add_assoc, hausdorffEDist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α))
⊢ infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α) =
    infEDist y (↑t : Set α) + (edist x y + hausdorffEDist (↑s : Set α) (↑t : Set α))
have 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 α))
Tactic: rw [add_assoc, hausdorffEDist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ 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))
have bc : edist x y ≤ edist (x, s) (y, t)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
bc : edist x y ≤ 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))
have bc₁ : hausdorffEDist (↑s : Set α) (↑t : Set α) ≤ edist (x, s) (y, t)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t)) =
    infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
have rw : infEDist y (↑t : Set α) + edist (x, s) (y, t) * 2 = infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
Tactic: rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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)
⊢ infEDist y (↑t : Set α) + (edist (x, s) (y, t) + edist (x, s) (y, t)) =
    infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
have rw₁ : infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t) = infEDist y (↑t : Set α) + 2 * edist (x, s) (y, t)
Tactic: rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist (x, s).1 (↑(x, s).2 : Set α) ≤ infEDist (y, t).1 (↑(y, t).2 : Set α) + 2 * edist (x, s) (y, t)
have infEDist : infEDist x (↑t : Set α) + hausdorffEDist (↑t : Set α) (↑s : Set α) ≤
  infEDist y (↑t : Set α) + edist x y + hausdorffEDist (↑t : Set α) (↑s : Set α)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ Metric.infEDist (x, s).1 (↑(x, s).2 : Set α) ≤ Metric.infEDist (y, t).1 (↑(y, t).2 : Set α) + 2 * edist (x, s) (y, t)
have 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 α))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α))
⊢ Metric.infEDist (x, s).1 (↑(x, s).2 : Set α) ≤ Metric.infEDist (y, t).1 (↑(y, t).2 : Set α) + 2 * edist (x, s) (y, t)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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))
⊢ Metric.infEDist (x, s).1 (↑(x, s).2 : Set α) ≤ Metric.infEDist (y, t).1 (↑(y, t).2 : Set α) + 2 * edist (x, s) (y, t)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ CompleteSpace.{u_1} (Closeds α)
have B_pos : ∀ (n : ℕ), 0 < B n
Tactic: have B_pos : ∀ n, (0 : ℝ≥0∞) < B n := by simp [B, ENNReal.pow_pos]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ CompleteSpace.{u_1} (Closeds α)
have B_ne_top : ∀ (n : ℕ), B n ≠ ∞
Tactic: have B_ne_top : ∀ n, B n ≠ ⊤ := by finiteness
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
have refine : ∀ (s : ℕ → Closeds α) (hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N),
  ∃ (x : Closeds α), Tendsto s atTop (𝓝 x)
Tactic: refine EMetric.complete_of_convergent_controlled_sequences B B_pos fun s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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' := ⋯ }
⊢ ∃ (x : Closeds α), Tendsto s atTop (𝓝 x)
have h : Tendsto s atTop (𝓝 t)
Tactic: use t
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
have refine : hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < B n / HPow.hPow (α := ℝ≥0∞) 2 l
Tactic: refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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))
⊢ hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < B n / HPow.hPow (α := ℝ≥0∞) 2 l
have simp : hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < B n * HPow.hPow (α := ℝ≥0∞) 2⁻¹ l
Tactic: simp only [ENNReal.inv_pow, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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))
⊢ hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < B n * HPow.hPow (α := ℝ≥0∞) 2⁻¹ l
have rw : hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + l)
Tactic: rw [← pow_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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))
⊢ hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + l)
have a : n + l ≤ n + l
Tactic: apply hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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))
a : n + l ≤ n + l
⊢ hausdorffEDist (↑(s (n + l)) : Set α) (↑(s (n + l + 1)) : Set α) < HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + l)
have a₁ : n + l ≤ n + l + 1
Tactic: apply hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
have obtain : ∀ (z' : α) (z'_mem : z' ∈ s (n + l + 1)) (hz' : edist (↑z : α) z' < B n / HPow.hPow (α := ℝ≥0∞) 2 l),
  ∃ (z' : ↥(s (n + l + 1))), edist (↑z : α) (↑z' : α) ≤ B n / HPow.hPow (α := ℝ≥0∞) 2 l
Tactic: obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l := by
          refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
          simp only [ENNReal.inv_pow, div_eq_mul_inv]
          rw [← pow_add]
          apply hs <;> simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ (z : (l : ℕ) → ↥(s (n + l))),
    (↑(z 0) : α) = x ∧ ∀ (k : ℕ), edist (↑(z k) : α) (↑(z (k + 1)) : α) ≤ B n / HPow.hPow (α := ℝ≥0∞) 2 k
have this : ∀ (l : ℕ) (z : ↥(s (n + l))), ∃ (z' : ↥(s (n + l + 1))), edist (↑z : α) (↑z' : α) ≤ B n / HPow.hPow (α := ℝ≥0∞) 2 l
Tactic: have : ∀ (l) (z : s (n + l)), ∃ z' : s (n + l + 1), edist (z : α) z' ≤ B n / 2 ^ l := by
        intro l z
        obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l := by
          refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
          simp only [ENNReal.inv_pow, div_eq_mul_inv]
          rw [← pow_add]
          apply hs <;> simp
        exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩