awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
inl :
  ∀ (hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hb : Bornology.IsBounded.{u} (α := α) ∅),
    IsCompact.{u} (X := α) ∅
⊢ IsCompact s
have inr : ∀ (x : α), IsCompact s
Tactic: rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
⊢ IsCompact s
have inr : ∀ (r : ℝ) (hr : s ⊆ closedBall x r), IsCompact s
Tactic: rcases hb.subset_closedBall x with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
have refine : Bornology.IsBounded s → BddBelow s ∧ BddAbove s
Tactic: refine ⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s → BddBelow s ∧ BddAbove s
have rw : (∃ (r : ℝ), s ⊆ closedBall x r) → BddBelow s ∧ BddAbove s
Tactic: rw [Metric.isBounded_iff_subset_closedBall x]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ Bornology.IsBounded.{u_3} (α := α) {x : α | |x| ≤ C}
have h : {x : α | |x| ≤ C} = Icc (-C) C
Tactic: convert! Metric.isBounded_Icc (-C) C
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ {x : α | |x| ≤ C} = Icc (-C) C
have h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | |x| ≤ C} x ↔ x ∈ Icc (-C) C
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ Bornology.IsBounded.{u_3} (α := α) {x : α | |x| < C}
have h : {x : α | |x| < C} = Ioo (-C) C
Tactic: convert! Metric.isBounded_Ioo (-C) C
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ {x : α | |x| < C} = Ioo (-C) C
have h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | |x| < C} x ↔ x ∈ Ioo (-C) C
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ diam (α := α) {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)
have simp : (max (max (edist x y) (edist x z)) (edist y z)).toReal =
  max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
Tactic: simp only [diam, ediam_triple, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
have hr : edist x y ≠ ∞
Tactic: rw [ENNReal.toReal_max, ENNReal.toReal_max]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
hr : edist x y ≠ ∞
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
have hp : edist x z ≠ ∞
Tactic: rw [ENNReal.toReal_max, ENNReal.toReal_max]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
hr : edist x y ≠ ∞
hp : edist x z ≠ ∞
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
have hr₁ : max (edist x y) (edist x z) ≠ ∞
Tactic: rw [ENNReal.toReal_max, ENNReal.toReal_max]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
hr : edist x y ≠ ∞
hp : edist x z ≠ ∞
hr₁ : max (edist x y) (edist x z) ≠ ∞
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal
have hp₁ : edist y z ≠ ∞
Tactic: rw [ENNReal.toReal_max, ENNReal.toReal_max]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ diam s
have rw : (edist x y).toReal ≤ (ediam s).toReal
Tactic: rw [diam, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ ediam.{u} (X := α) univ = ∞ ↔ NoncompactSpace α
have rw : ediam.{u} (X := α) univ = ∞ ↔ ¬CompactSpace α
Tactic: rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
rw : ediam.{u} (X := α) univ = ∞ ↔ ¬CompactSpace α
⊢ ediam.{u} (X := α) univ = ∞ ↔ NoncompactSpace α
have rw₁ : ediam.{u} (X := α) univ = ∞ ↔ ¬Bornology.IsBounded.{u} (α := α) univ
Tactic: rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
rw : ediam.{u} (X := α) univ = ∞ ↔ ¬CompactSpace α
rw₁ : ediam.{u} (X := α) univ = ∞ ↔ ¬Bornology.IsBounded.{u} (α := α) univ
⊢ ediam.{u} (X := α) univ = ∞ ↔ NoncompactSpace α
have rw₂ : ediam.{u} (X := α) univ = ∞ ↔ ¬ediam.{u} (X := α) univ ≠ ∞
Tactic: rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
rw : ediam.{u} (X := α) univ = ∞ ↔ ¬CompactSpace α
rw₁ : ediam.{u} (X := α) univ = ∞ ↔ ¬Bornology.IsBounded.{u} (α := α) univ
rw₂ : ediam.{u} (X := α) univ = ∞ ↔ ¬ediam.{u} (X := α) univ ≠ ∞
⊢ ediam.{u} (X := α) univ = ∞ ↔ NoncompactSpace α
have rw₃ : ediam.{u} (X := α) univ = ∞ ↔ ediam.{u} (X := α) univ = ∞
Tactic: rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ diam s = 0
have rw : (ediam s).toReal = 0
Tactic: rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
rw : (ediam s).toReal = 0
⊢ diam s = 0
have rw₁ : ENNReal.toReal ∞ = 0
Tactic: rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
rw : (ediam s).toReal = 0
rw₁ : ENNReal.toReal ∞ = 0
⊢ diam s = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t
have simp : (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal
Tactic: simp only [diam, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal
have hb : ediam s + edist x y = ∞ → ediam (s ∪ t) = ∞
Tactic: grw [ENNReal.toReal_le_add' (ediam_union_le_add_edist xs yt), ENNReal.toReal_add_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
hb : ediam s + edist x y = ∞ → ediam (s ∪ t) = ∞
⊢ (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal
have hc : ediam t = ∞ → ediam (s ∪ t) = ∞
Tactic: grw [ENNReal.toReal_le_add' (ediam_union_le_add_edist xs yt), ENNReal.toReal_add_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s + edist x y = ∞ → ediam (s ∪ t) = ∞
have hb : ediam s = ∞ → ediam (s ∪ t) = ∞
Tactic: simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
⊢ diam (s ∪ t) ≤ diam s + diam t
have rcases : ∀ (x : α) (xs : x ∈ s) (xt : x ∈ t), diam (s ∪ t) ≤ diam s + diam t
Tactic: rcases h with ⟨x, ⟨xs, xt⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n
have apply : ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n ⊆ s n
Tactic: apply mem_of_subset_of_mem _ (h N).choose_spec
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
n N : ℕ
hn : n ≤ N
x : α
hx : Membership.mem (γ := Set α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n) x
⊢ x ∈ s n
have hx₁ : ∀ (i : ℕ) (i_1 : i ≤ N), x ∈ s i
Tactic: simp only [mem_iInter] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
have I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
Tactic: have I : ∀ n N, n ≤ N → u N ∈ s n := by
    intro n N hn
    apply mem_of_subset_of_mem _ (h N).choose_spec
    intro x hx
    simp only [mem_iInter] at hx
    exact hx n hn
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ CauchySeq u
have apply : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ diam (s N)
Tactic: apply cauchySeq_of_le_tendsto_0 _ _ h'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
have this : CauchySeq u
Tactic: have : CauchySeq u := by
    apply cauchySeq_of_le_tendsto_0 _ _ h'
    intro m n N hm hn
    exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
have obtain : ∀ (x : α) (xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
Tactic: obtain ⟨x, -, xlim⟩ : ∃ x ∈ s 0, Tendsto (fun n : ℕ => u n) atTop (𝓝 x) :=
    cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n zero_le) this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
have refine : ∀ (n : ℕ), x ∈ s n
Tactic: refine ⟨x, mem_iInter.2 fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n : ℕ
⊢ x ∈ s n
have apply : ∀ᶠ (x : ℕ) in atTop, u x ∈ s n
Tactic: apply (hs n).mem_of_tendsto xlim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, u x ∈ s n
have h₁ : ∀ (p : ℕ) (hp : p ∈ Ici n), u p ∈ s n
Tactic: filter_upwards [Ici_mem_atTop n] with p hp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
s : Set α
inst : MetricSpace α
hs1 : s.Nontrivial
hs2 : Bornology.IsBounded s
⊢ 0 < diam s
have rcases : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), 0 < diam s
Tactic: rcases hs1 with ⟨x, hx, y, hy, hxy⟩
Cleared hypotheses: hs1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ cobounded α = cocompact α
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
h : Nontrivial α
⊢ cobounded α = cocompact α
have inhabit : ∀ (inhabited_h : Inhabited α), cobounded α = cocompact α
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (K ∩ s).Finite
have refine_1 : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)
Tactic: refine (IsCompact.finite ?_ ?_).subset (Set.inter_subset_inter_left s subset_closure)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
refine_1 : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)
⊢ (K ∩ s).Finite
have refine_2 : IsDiscrete (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)
Tactic: refine (IsCompact.finite ?_ ?_).subset (Set.inter_subset_inter_left s subset_closure)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y
have refine : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
Tactic: refine hf.exists_forall_le' (x₀ := x₀) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ {x : β | f x₀ < f x} ∈ cocompact β
have refine : IsCompact.{u_4} (X := β) {x : β | f x₀ < f x}ᶜ
Tactic: refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ IsCompact.{u_4} (X := β) {x : β | f x₀ < f x}ᶜ
have simp : IsCompact.{u_4} (X := β) {a : β | f a ≤ f x₀}
Tactic: simp only [Set.compl_setOf, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
have hU : {x : β | f x₀ < f x} ∈ cocompact β
Tactic: have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β := by
    refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
    simp only [Set.compl_setOf, not_lt]
    exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
hU : {x : β | f x₀ < f x} ∈ cocompact β
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
have h₁ : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | f x₀ < f x} x →
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f x₀ ≤ f x) x} x}
    a
Tactic: filter_upwards [hU] with x hx using hx.le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Bounded (goal)
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
hU : {x : β | f x₀ < f x} ∈ cocompact β
h₁ :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | f x₀ < f x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f x₀ ≤ f x) x} x}
      a
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
have h₂ : ∀ (a : β), f x₀ < f a → f x₀ ≤ f a
Tactic: filter_upwards [hU] with x hx using hx.le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ (d : (a : X) → X → R) x z ⊔ (d' : (a : X) → X → R) x z ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have simp : (d : (a : X) → X → R) x z ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R) ∧
  (d' : (a : X) → X → R) x z ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
Tactic: simp only [sup_le_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.BundledFun (goal)
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ (d : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R) ∧
    (d' : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
have refine_1 : HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y z : R) ≤
  HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
    ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
Tactic: refine ⟨(d.triangle x y z).trans ?_, (d'.triangle x y z).trans ?_⟩