awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ Bornology.IsBounded (Ioo a b)

Tactic:
(totallyBounded_Ioo a b).isBounded

Premises used: totallyBounded_Ioo, TotallyBounded.isBounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
s : Set α
h₁ : BddAbove s
h₂ : BddBelow s
⊢ Bornology.IsBounded s

Tactic:
let ⟨u, hu⟩ := h₁
  let ⟨l, hl⟩ := h₂
  (isBounded_Icc l u).subset (fun _x hx => mem_Icc.mpr ⟨hl hx, hu hx⟩)

Premises used: Iff.mpr, _private.0.Metric.isBounded_of_bddAbove_of_bddBelow.match_1, _private.0.Metric.isBounded_of_bddAbove_of_bddBelow.match_2, Bornology.IsBounded, Bornology.IsBounded.subset, And.intro, Set.mem_Icc, Metric.isBounded_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
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

Tactic:
⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩

Premises used: Metric.isBounded_of_bddAbove_of_bddBelow, And.right, And.left, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 α
refine : Bornology.IsBounded s → BddBelow s ∧ BddAbove s
⊢ Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
refine ⟨?_, fun hs ↦ Metric.isBounded_of_bddAbove_of_bddBelow hs.2 hs.1⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 α
rw : (∃ (r : ℝ), s ⊆ closedBall x r) → BddBelow s ∧ BddAbove s
⊢ Bornology.IsBounded s → BddBelow s ∧ BddAbove s

Tactic:
rw [Metric.isBounded_iff_subset_closedBall x]

Premises used: Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 α
r : ℝ
hr : s ⊆ closedBall x r
⊢ BddBelow s ∧ BddAbove s

Tactic:
⟨(bddBelow_ball _).mono hr, (bddAbove_ball _).mono hr⟩

Premises used: BddBelow.mono, And.intro, BddAbove.mono
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 α
r : ℝ
hr : s ⊆ closedBall x r
⊢ BddBelow s ∧ BddAbove s

Tactic:
exact ⟨(bddBelow_ball _).mono hr, (bddAbove_ball _).mono hr⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ Bornology.IsBounded (Icc (-C) C)

Tactic:
Metric.isBounded_Icc (-C) C

Premises used: Metric.isBounded_Icc, Neg.neg
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
h : {x : α | |x| ≤ C} = Icc (-C) C
⊢ Bornology.IsBounded.{u_3} (α := α) {x : α | |x| ≤ C}

Tactic:
convert! Metric.isBounded_Icc (-C) C

Premises used: Metric.isBounded_Icc, Neg.neg
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | |x| ≤ C} x ↔ x ∈ Icc (-C) C
⊢ {x : α | |x| ≤ C} = Icc (-C) C

Tactic:
ext1 x
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C x : α
⊢ Membership.mem (γ := Set α) {x : α | |x| ≤ C} x ↔ x ∈ Icc (-C) C

Tactic:
simp [abs_le]

Premises used: abs_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
⊢ Bornology.IsBounded (Ioo (-C) C)

Tactic:
Metric.isBounded_Ioo (-C) C

Premises used: Metric.isBounded_Ioo, Neg.neg
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
h : {x : α | |x| < C} = Ioo (-C) C
⊢ Bornology.IsBounded.{u_3} (α := α) {x : α | |x| < C}

Tactic:
convert! Metric.isBounded_Ioo (-C) C

Premises used: Metric.isBounded_Ioo, Neg.neg
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C : α
h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | |x| < C} x ↔ x ∈ Ioo (-C) C
⊢ {x : α | |x| < C} = Ioo (-C) C

Tactic:
ext1 x
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : PseudoMetricSpace α
inst_4 : CompactIccSpace α
C x : α
⊢ Membership.mem (γ := Set α) {x : α | |x| < C} x ↔ x ∈ Ioo (-C) C

Tactic:
simp [abs_lt]

Premises used: abs_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
⊢ 0 ≤ diam s

Tactic:
ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
hs : s.Subsingleton
⊢ diam s = 0

Tactic:
simp [diam, ediam_subsingleton hs]

Premises used: Metric.ediam_subsingleton, Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ diam.{u} (α := α) ∅ = 0

Tactic:
diam_subsingleton subsingleton_empty

Premises used: Set.subsingleton_empty, Metric.diam_subsingleton
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
inst : PseudoMetricSpace α
⊢ diam (α := α) {x} = 0

Tactic:
diam_subsingleton subsingleton_singleton

Premises used: Set.subsingleton_singleton, Metric.diam_subsingleton
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : One α
⊢ diam.{u} (α := α) 1 = 0

Tactic:
diam_singleton

Premises used: Metric.diam_singleton
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y : α
inst : PseudoMetricSpace α
⊢ diam (α := α) {x, y} = dist x y

Tactic:
simp only [diam, ediam_pair, dist_edist]

Premises used: Metric.ediam_pair, Metric.diam, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
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
⊢ diam (α := α) {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

Tactic:
simp only [diam, ediam_triple, dist_edist]

Premises used: Metric.ediam_triple, Metric.diam, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
hr : edist x y ≠ ∞
hp : edist x z ≠ ∞
hr₁ : max (edist x y) (edist x z) ≠ ∞
hp₁ : edist y 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

Tactic:
rw [ENNReal.toReal_max, ENNReal.toReal_max]

Premises used: ENNReal.toReal_max
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ edist x y ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

Premises used: max_lt, edist_lt_top, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ edist x z ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

Premises used: max_lt, edist_lt_top, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

Premises used: max_lt, edist_lt_top, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x y z : α
inst : PseudoMetricSpace α
⊢ edist y z ≠ ∞

Tactic:
apply_rules [ne_of_lt, edist_lt_top, max_lt]

Premises used: max_lt, edist_lt_top, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
C : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C
⊢ ediam s ≤ ENNReal.ofReal C

Tactic:
ediam_le fun x hx y hy => (edist_dist x y).symm ▸ ENNReal.ofReal_le_ofReal (h x hx y hy)

Premises used: ENNReal.ofReal_le_ofReal, Eq.rec, edist_dist, Metric.ediam_le, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
C : ℝ
h₀ : 0 ≤ C
h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C
⊢ diam s ≤ C

Tactic:
ENNReal.toReal_le_of_le_ofReal h₀ (ediam_le_of_forall_dist_le h)

Premises used: Metric.ediam_le_of_forall_dist_le, Metric.diam, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
hs : s.Nonempty
C : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C
⊢ diam s ≤ C

Tactic:
have h₀ : 0 ≤ C :=
    let ⟨x, hx⟩ := hs
    le_trans dist_nonneg (h x hx x hx)
  diam_le_of_forall_dist_le h₀ h

Premises used: dist_nonneg, _private.0.Metric.diam_le_of_forall_dist_le_of_nonempty.match_1, LE.le, OfNat.ofNat, Metric.diam_le_of_forall_dist_le, le_trans
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
rw : (edist x y).toReal ≤ (ediam s).toReal
⊢ dist x y ≤ diam s

Tactic:
rw [diam, dist_edist]

Premises used: Metric.diam, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (ediam s).toReal

Tactic:
ENNReal.toReal_mono h <| edist_le_ediam_of_mem hx hy

Premises used: Metric.edist_le_ediam_of_mem, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (ediam s).toReal

Tactic:
exact ENNReal.toReal_mono h <| edist_le_ediam_of_mem hx hy

Premises used: Metric.edist_le_ediam_of_mem, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
⊢ Bornology.IsBounded s ↔ ediam s ≠ ∞

Tactic:
isBounded_iff.trans <| Iff.intro
    (fun ⟨_C, hC⟩ => ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| ediam_le_of_forall_dist_le hC)
    fun h => ⟨diam s, fun _x hx _y hy => dist_le_diam_of_mem' h hx hy⟩

Premises used: Metric.isBounded_iff, Ne, _private.0.Metric.isBounded_closure_of_isBounded.match_1, Metric.ediam, ne_top_of_le_ne_top, Iff.intro, Exists.intro, Metric.ediam_le_of_forall_dist_le, Iff.trans, Metric.diam, ENNReal.ofReal_ne_top, Metric.dist_le_diam_of_mem', Top.top
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
⊢ ediam s = ∞ ↔ ¬Bornology.IsBounded s

Tactic:
isBounded_iff_ediam_ne_top.not_left.symm

Premises used: Metric.isBounded_iff_ediam_ne_top, Iff.not_left, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 ≠ ∞
rw₃ rw₄ : ediam.{u} (X := α) univ = ∞ ↔ ediam.{u} (X := α) univ = ∞
⊢ ediam.{u} (X := α) univ = ∞ ↔ NoncompactSpace α

Tactic:
rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]

Premises used: Classical.not_not, Metric.isBounded_iff_ediam_ne_top, not_compactSpace_iff, Metric.compactSpace_iff_isBounded_univ
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : NoncompactSpace α
⊢ ediam.{u} (X := α) univ = ∞

Tactic:
ediam_univ_eq_top_iff_noncompact.mpr ‹_›

Premises used: Iff.mpr, Metric.ediam_univ_eq_top_iff_noncompact
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
inst_2 : NoncompactSpace α
⊢ diam.{u} (α := α) univ = 0

Tactic:
simp [diam]

Premises used: Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ diam s

Tactic:
dist_le_diam_of_mem' h.ediam_ne_top hx hy

Premises used: Bornology.IsBounded.ediam_ne_top, Metric.dist_le_diam_of_mem'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ ediam s = ∞

Tactic:
ediam_eq_top_iff_unbounded.2 h

Premises used: Iff.mpr, Metric.ediam_eq_top_iff_unbounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
rw : (ediam s).toReal = 0
rw₁ : ENNReal.toReal ∞ = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ diam s = 0

Tactic:
rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]

Premises used: Metric.ediam_of_unbounded, Metric.diam, ENNReal.toReal_top
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s t : Set α
h : s ⊆ t
ht : Bornology.IsBounded t
⊢ diam s ≤ diam t

Tactic:
ENNReal.toReal_mono ht.ediam_ne_top <| ediam_mono h

Premises used: Bornology.IsBounded.ediam_ne_top, Metric.ediam_mono, Metric.diam, ENNReal.toReal_mono
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
simp : (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t

Tactic:
simp only [diam, dist_edist]

Premises used: Metric.diam, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Bounded
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) = ∞
hc : ediam t = ∞ → ediam (s ∪ t) = ∞
⊢ (ediam (s ∪ t)).toReal ≤ (ediam s).toReal + (edist x y).toReal + (ediam t).toReal

Tactic:
grw [ENNReal.toReal_le_add' (ediam_union_le_add_edist xs yt), ENNReal.toReal_add_le]

Premises used: ENNReal.toReal_add_le, Metric.ediam_union_le_add_edist, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
hb : ediam s = ∞ → ediam (s ∪ t) = ∞
⊢ ediam s + edist x y = ∞ → ediam (s ∪ t) = ∞

Tactic:
simp only [ENNReal.add_eq_top, edist_ne_top, or_false]

Premises used: ENNReal.add_eq_top, edist_ne_top, or_false
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s = ∞ → ediam (s ∪ t) = ∞

Tactic:
fun h ↦ top_unique <| h ▸ ediam_mono subset_union_left

Premises used: Eq.rec, Metric.ediam_mono, Set.subset_union_left, top_unique
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam s = ∞ → ediam (s ∪ t) = ∞

Tactic:
exact fun h ↦ top_unique <| h ▸ ediam_mono subset_union_left

Premises used: top_unique
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam t = ∞ → ediam (s ∪ t) = ∞

Tactic:
fun h ↦ top_unique <| h ▸ ediam_mono subset_union_right

Premises used: Set.subset_union_right, Eq.rec, Metric.ediam_mono, top_unique
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x y : α
inst : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ediam t = ∞ → ediam (s ∪ t) = ∞

Tactic:
exact fun h ↦ top_unique <| h ▸ ediam_mono subset_union_right

Premises used: top_unique
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
rcases : ∀ (x : α) (xs : x ∈ s) (xt : x ∈ t), diam (s ∪ t) ≤ diam s + diam t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
rcases h with ⟨x, ⟨xs, xt⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
simpa using diam_union xs xt

Premises used: Metric.diam_union
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
x : α
inst : PseudoMetricSpace α
r : ℝ
hr : 0 ≤ r
h : s ⊆ closedBall x r
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ r + r = 2 * r

Tactic:
simp [mul_two, mul_comm]

Premises used: mul_comm, mul_two
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
inst : PseudoMetricSpace α
r : ℝ
h : 0 ≤ r
⊢ diam (closedBall x r) ≤ 2 * r

Tactic:
diam_le_of_subset_closedBall h Subset.rfl

Premises used: Metric.diam_le_of_subset_closedBall, Set.Subset.rfl
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
inst : PseudoMetricSpace α
r : ℝ
h : 0 ≤ r
⊢ diam (ball x r) ≤ 2 * r

Tactic:
diam_le_of_subset_closedBall h ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Metric.diam_le_of_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
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
apply : ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n ⊆ s n
⊢ u N ∈ s n

Tactic:
apply mem_of_subset_of_mem _ (h N).choose_spec

Premises used: Exists.choose_spec, Set.mem_of_subset_of_mem
-- Module: Mathlib.Topology.MetricSpace.Bounded
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
⊢ ∀ (i : ℕ) (i_1 : i ≤ N), x ∈ s i

Tactic:
simp only [mem_iInter] at hx

Premises used: Set.mem_iInter
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 : ∀ (i : ℕ) (i_1 : i ≤ N), x ∈ s i
⊢ x ∈ s n

Tactic:
hx n hn
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 : ∀ (i : ℕ) (i_1 : i ≤ N), x ∈ s i
⊢ x ∈ s n

Tactic:
exact hx n hn
-- Module: Mathlib.Topology.MetricSpace.Bounded
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 : ℕ), 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
-- Module: Mathlib.Topology.MetricSpace.Bounded
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
apply : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ diam (s N)
⊢ CauchySeq u

Tactic:
apply cauchySeq_of_le_tendsto_0 _ _ h'

Premises used: cauchySeq_of_le_tendsto_0
-- Module: Mathlib.Topology.MetricSpace.Bounded
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
m n N : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ dist (u m) (u n) ≤ diam (s N)

Tactic:
dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)

Premises used: Metric.dist_le_diam_of_mem
-- Module: Mathlib.Topology.MetricSpace.Bounded
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
m n N : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ dist (u m) (u n) ≤ diam (s N)

Tactic:
exact dist_le_diam_of_mem (h's N) (I _ _ hm) (I _ _ hn)

Premises used: Metric.dist_le_diam_of_mem
-- Module: Mathlib.Topology.MetricSpace.Bounded
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

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)