awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, dist_triangle]

Premises used: PseudoMetricSpace.dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), edist x y = ENNReal.ofReal (d x y)

Tactic:
simp [hd, edist_dist]

Premises used: PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ 𝓤 X = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : X × X | d p.1 p.2 < ε}

Tactic:
simp [hd, uniformity_dist]

Premises used: PseudoMetricSpace.uniformity_dist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ (cobounded X).sets = {s : Set X | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, d x y ≤ C}

Tactic:
simp [hd, cobounded_sets]

Premises used: PseudoMetricSpace.cobounded_sets
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
h : Eq.{u_2 + 1} (α := X → X → ℝ) dist dist
⊢ m.replaceDist d hd = m

Tactic:
ext : 2
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ) dist dist

Tactic:
hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ) dist dist

Tactic:
exact hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := UniformSpace X) toUniformSpace toUniformSpace

Tactic:
dsimp +instances [replaceDist]

Premises used: PseudoMetricSpace.replaceDist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := Bornology X) toBornology toBornology

Tactic:
dsimp +instances [replaceDist]

Premises used: PseudoMetricSpace.replaceDist
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, edist_triangle]

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
h : Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist
⊢ m.replaceEDist d hd = m

Tactic:
ext : 2
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist

Tactic:
hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ≥0∞) edist edist

Tactic:
exact hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ Eq.{u_2 + 1} (α := UniformSpace X) PseudoEMetricSpace.toUniformSpace PseudoEMetricSpace.toUniformSpace

Tactic:
simp +instances [replaceEDist_eq]

Premises used: EMetricSpace.replaceEDist_eq
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
simp [hd, dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
simp [hd, dist_triangle]

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
simp [hd]
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
h : Eq.{u_2 + 1} (α := X → X → ℝ) dist dist
⊢ m.replaceDist d hd = m

Tactic:
ext : 2
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ) dist dist

Tactic:
hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := X → X → ℝ) dist dist

Tactic:
exact hd
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := UniformSpace X) PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace

Tactic:
simp +instances [replaceDist_eq]

Premises used: MetricSpace.replaceDist_eq
-- Module: Mathlib.Topology.MetricSpace.Basic
Goal:
α : Type u
β : Type v
X_1 : Type u_1
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ Eq.{u_2 + 1} (α := Bornology X) PseudoMetricSpace.toBornology PseudoMetricSpace.toBornology

Tactic:
simp +instances [replaceDist_eq]

Premises used: MetricSpace.replaceDist_eq
-- Module: Mathlib.Topology.MetricSpace.Bilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K₁ K₂ : ℝ≥0
f : α → β
hf₁ : AntilipschitzWith K₁ f
hf₂ : LipschitzWith K₂ f
⊢ 𝓤 α = 𝓤 α

Tactic:
hf₁.isUniformInducing hf₂.uniformContinuous |>.comap_uniformity

Premises used: IsUniformInducing.comap_uniformity, Set.Mem, uniformity, setOf, AntilipschitzWith.isUniformInducing, LipschitzWith.uniformContinuous, Filter.comap
-- Module: Mathlib.Topology.MetricSpace.Bilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K₁ K₂ : ℝ≥0
f : α → β
hf₁ : AntilipschitzWith K₁ f
hf₂ : LipschitzWith K₂ f
⊢ cobounded α = cobounded α

Tactic:
le_antisymm hf₂.comap_cobounded_le hf₁.tendsto_cobounded.le_comap

Premises used: Filter.Tendsto.le_comap, AntilipschitzWith.tendsto_cobounded, LipschitzWith.comap_cobounded_le, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Bilipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K₁ K₂ : ℝ≥0
f : α → β
hf₁ : AntilipschitzWith K₁ f
hf₂ : LipschitzWith K₂ f
s : Set α
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
Filter.ext_iff.1 (bornology_eq_of_bilipschitz hf₁ hf₂) (sᶜ)

Premises used: Compl.compl, bornology_eq_of_bilipschitz, Bornology.IsBounded, Filter.ext_iff, Iff.mp, Bornology.IsCobounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : UniformSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ TotallyBounded (Icc a b)

Tactic:
isCompact_Icc.totallyBounded

Premises used: IsCompact.totallyBounded, CompactIccSpace.isCompact_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : UniformSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ TotallyBounded (Ico a b)

Tactic:
(totallyBounded_Icc a b).subset Ico_subset_Icc_self

Premises used: TotallyBounded.subset, Set.Ico_subset_Icc_self, totallyBounded_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : UniformSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ TotallyBounded (Ioc a b)

Tactic:
(totallyBounded_Icc a b).subset Ioc_subset_Icc_self

Premises used: TotallyBounded.subset, Set.Ioc_subset_Icc_self, totallyBounded_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : UniformSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ TotallyBounded (Ioo a b)

Tactic:
(totallyBounded_Icc a b).subset Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, TotallyBounded.subset, totallyBounded_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
r : ℝ
inst : PseudoMetricSpace α
⊢ Bornology.IsBounded (closedBall x r)

Tactic:
isBounded_iff.2 ⟨r + r, fun y hy z hz =>
    calc dist y z ≤ dist y x + dist z x := dist_triangle_right _ _ _
    _ ≤ r + r := add_le_add hy hz⟩

Premises used: Iff.mpr, Trans.trans, add_le_add, dist_triangle_right, Metric.isBounded_iff, HAdd.hAdd, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
r : ℝ
inst : PseudoMetricSpace α
⊢ Bornology.IsBounded (ball x r)

Tactic:
isBounded_closedBall.subset ball_subset_closedBall

Premises used: Metric.isBounded_closedBall, Metric.ball_subset_closedBall, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
inl :
  ∀ (hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
    ∃ (f : ℕ → Set α),
      Monotone f ∧
        Eq.{u + 1} (α := Set α) (⋃ (i : ℕ), f i) ∅ ∧
          ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
inr :
  ∀ (x : α),
    ∃ (f : ℕ → Set α),
      Monotone f ∧
        ⋃ (i : ℕ), f i = U ∧
          ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
obtain rfl | ⟨x, -⟩ := U.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ Eq.{u + 1} (α := Set α) (⋃ (i : ℕ), (fun (i : ℕ) ↦ (∅ : Set α)) i) ∅ ∧
    ∀ (i : ℕ),
      Bornology.IsBounded.{u} (α := α) ((fun (i : ℕ) ↦ (∅ : Set α)) i) ∧
        IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((fun (i : ℕ) ↦ (∅ : Set α)) i)

Tactic:
simp_all
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      Eq.{u + 1} (α := Set α) (⋃ (i : ℕ), f i) ∅ ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
exact ⟨fun i ↦ ∅, monotone_const, by simp_all⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩

Premises used: Metric.ball, Nat.cast, Inter.inter, Metric.isOpen_ball, And.intro, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
inr :
  ∀ (i j : ℕ) (hij : i ≤ j),
    LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)
inr₁ : ⋃ (i : ℕ), (fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i = U
inr₂ : ∀ (i : ℕ), Bornology.IsBounded.{u} (α := α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i)
⊢ ∃ (f : ℕ → Set α),
    Monotone f ∧
      ⋃ (i : ℕ), f i = U ∧
        ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)

Tactic:
refine ⟨fun i ↦ U ∩ ball x i, fun i j hij ↦ ?_, ?_, fun i ↦ ⟨?_, hU.inter isOpen_ball⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
i j : ℕ
hij : i ≤ j
⊢ LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)

Tactic:
inter_subset_inter_right _ (ball_subset_ball (Nat.cast_le.2 hij))

Premises used: Iff.mpr, Set.inter_subset_inter_right, Metric.ball_subset_ball, Nat.cast_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
i j : ℕ
hij : i ≤ j
⊢ LE.le.{u} (α := Set α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) j)

Tactic:
exact inter_subset_inter_right _ (ball_subset_ball (Nat.cast_le.2 hij))

Premises used: Iff.mpr, Set.inter_subset_inter_right, Metric.ball_subset_ball, Nat.cast_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
⊢ ⋃ (i : ℕ), (fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i = U

Tactic:
simp [← inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
i : ℕ
⊢ Bornology.IsBounded.{u} (α := α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i)

Tactic:
isBounded_ball.subset inter_subset_right

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
x : α
i : ℕ
⊢ Bornology.IsBounded.{u} (α := α) ((fun (i : ℕ) ↦ U ∩ ball x (↑i : ℝ)) i)

Tactic:
exact isBounded_ball.subset inter_subset_right

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
x : α
r : ℝ
inst : PseudoMetricSpace α
⊢ Bornology.IsBounded (sphere x r)

Tactic:
isBounded_closedBall.subset sphere_subset_closedBall

Premises used: Metric.isBounded_closedBall, Bornology.IsBounded.subset, Metric.sphere_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
c : α
⊢ Bornology.IsBounded s ↔ ∃ (r : ℝ), s ⊆ closedBall c r

Tactic:
⟨fun h ↦ (isBounded_iff.1 (h.insert c)).imp fun _r hr _x hx ↦ hr (.inr hx) (mem_insert _ _),
    fun ⟨_r, hr⟩ ↦ isBounded_closedBall.subset hr⟩

Premises used: Metric.isBounded_closedBall, Metric.isBounded_iff, Bornology.IsBounded, Bornology.IsBounded.insert, Exists.imp, _private.0.Metric.isBounded_iff_subset_closedBall.match_1, Bornology.IsBounded.subset, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
c : α
⊢ ∃ (r : ℝ), s ⊆ closedBall c r

Tactic:
(isBounded_iff_subset_closedBall c).1 h

Premises used: Iff.mp, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
a : ℝ
c : α
⊢ ∃ (r : ℝ), a < r ∧ s ⊆ ball c r

Tactic:
let ⟨r, hr⟩ := h.subset_closedBall c
  ⟨max r a + 1, (le_max_right _ _).trans_lt (lt_add_one _), hr.trans <| closedBall_subset_ball <|
    (le_max_left _ _).trans_lt (lt_add_one _)⟩

Premises used: le_max_right, lt_add_one, Exists, Metric.closedBall_subset_ball, HasSubset.Subset.trans, Metric.ball, HasSubset.Subset, _private.0.Metric.isBounded_iff_subset_closedBall.match_1, Bornology.IsBounded.subset_closedBall, And, HAdd.hAdd, Max.max, And.intro, LT.lt, Exists.intro, OfNat.ofNat, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
c : α
⊢ ∃ (r : ℝ), s ⊆ ball c r

Tactic:
(h.subset_ball_lt 0 c).imp fun _ ↦ And.right

Premises used: Bornology.IsBounded.subset_ball_lt, Exists.imp, And.right, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
c : α
⊢ Bornology.IsBounded s ↔ ∃ (r : ℝ), s ⊆ ball c r

Tactic:
⟨(IsBounded.subset_ball · c), fun ⟨_r, hr⟩ ↦ isBounded_ball.subset hr⟩

Premises used: Metric.isBounded_ball, _private.0.Metric.isBounded_iff_subset_ball.match_1, Bornology.IsBounded, Bornology.IsBounded.subset_ball, Bornology.IsBounded.subset, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
a : ℝ
c : α
⊢ ∃ (r : ℝ), a < r ∧ s ⊆ closedBall c r

Tactic:
let ⟨r, har, hr⟩ := h.subset_ball_lt a c
  ⟨r, har, hr.trans ball_subset_closedBall⟩

Premises used: Metric.ball_subset_closedBall, _private.0.Bornology.IsBounded.subset_closedBall_lt.match_1, Exists, HasSubset.Subset.trans, HasSubset.Subset, Bornology.IsBounded.subset_ball_lt, And, And.intro, LT.lt, Exists.intro, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
⊢ Bornology.IsBounded (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
let ⟨C, h⟩ := isBounded_iff.1 h
  isBounded_iff.2 ⟨C, fun _a ha _b hb => isClosed_Iic.closure_subset <|
    map_mem_closure₂ continuous_dist ha hb h⟩

Premises used: Iff.mpr, map_mem_closure₂, continuous_dist, Metric.isBounded_iff, Bornology.IsBounded, _private.0.Metric.isBounded_closure_of_isBounded.match_1, isClosed_Iic, closure, IsClosed.closure_subset, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
h : Bornology.IsBounded s
⊢ Bornology.IsBounded (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
isBounded_closure_of_isBounded h

Premises used: Metric.isBounded_closure_of_isBounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
⊢ Bornology.IsBounded (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔ Bornology.IsBounded s

Tactic:
⟨fun h => h.subset subset_closure, fun h => h.closure⟩

Premises used: subset_closure, Bornology.IsBounded.subset, Iff.intro, Bornology.IsBounded.closure
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
simp_rw :
  (𝓝 x).HasBasis
    (fun (a : Set α) ↦ (x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) ∧ Bornology.IsBounded a)
    id
⊢ (𝓝 x).HasBasis
    (fun (a : Set α) ↦ x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧ Bornology.IsBounded a) id

Tactic:
simp_rw [← and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
apply :
  ∀ (s : Set α) (hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    ∃ (j : Set α),
      (x ∈ j ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] j) ∧ Bornology.IsBounded j ∧ j ⊆ s
⊢ (𝓝 x).HasBasis
    (fun (a : Set α) ↦ (x ∈ a ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a) ∧ Bornology.IsBounded a)
    id

Tactic:
apply (nhds_basis_opens x).restrict fun s hs ↦ ?_

Premises used: Filter.HasBasis.restrict, nhds_basis_opens
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ∩ ball x 1 ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ ball x 1)

Tactic:
aesop (add safe apply IsOpen.inter)

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Bornology.IsBounded (s ∩ ball x 1) ∧ s ∩ ball x 1 ⊆ s

Tactic:
simpa using Metric.isBounded_ball.subset Set.inter_subset_right

Premises used: Metric.isBounded_ball, Bornology.IsBounded.subset, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s : Set α
hs : x ∈ s ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ∃ (j : Set α), (x ∈ j ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] j) ∧ Bornology.IsBounded j ∧ j ⊆ s

Tactic:
exact ⟨s ∩ Metric.ball x 1,
    by aesop (add safe apply IsOpen.inter),
    by simpa using Metric.isBounded_ball.subset Set.inter_subset_right⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
x : Set α
⊢ (∃ (r : ℝ), x ⊆ closedBall c r) ↔ ∃ (i : ℝ), True ∧ (closedBall c i)ᶜ ⊆ xᶜ

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
x x_1 : ℝ
hr : x ≤ x_1
x_2 : α
⊢ x_2 ∈ (closedBall c x_1)ᶜ → x_2 ∈ (closedBall c x)ᶜ

Tactic:
simpa using hr.trans_lt

Premises used: LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
x : Set α
⊢ (∃ (r : ℝ), x ⊆ ball c r) ↔ ∃ (i : ℝ), True ∧ (ball c i)ᶜ ⊆ xᶜ

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
x x_1 : ℝ
hr : x ≤ x_1
x_2 : α
⊢ x_2 ∈ (ball c x_1)ᶜ → x_2 ∈ (ball c x)ᶜ

Tactic:
simpa using hr.trans

Premises used: LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
⊢ (cobounded α).HasBasis (fun (x : ℝ) ↦ True) fun (i : ℝ) ↦ (fun (x : α) ↦ dist x c) ⁻¹' Ici i

Tactic:
simpa only [compl_def, mem_ball, not_lt] using hasBasis_cobounded_compl_ball c

Premises used: Set.compl_def, Metric.hasBasis_cobounded_compl_ball, Metric.mem_ball, not_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
⊢ comap (dist c) atTop = cobounded α

Tactic:
simpa only [dist_comm _ c] using comap_dist_right_atTop c

Premises used: Metric.comap_dist_right_atTop, dist_comm