awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁

Tactic:
dist_lt_add_of_nonempty_closedBall_inter_ball h

Premises used: Metric.dist_lt_add_of_nonempty_closedBall_inter_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁

Tactic:
exact dist_lt_add_of_nonempty_closedBall_inter_ball h

Premises used: Metric.dist_lt_add_of_nonempty_closedBall_inter_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (ball x ε₁ ∩ ball y ε₂).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
dist_lt_add_of_nonempty_closedBall_inter_ball <|
    h.mono (inter_subset_inter ball_subset_closedBall Subset.rfl)

Premises used: Metric.ball_subset_closedBall, Set.inter_subset_inter, Metric.dist_lt_add_of_nonempty_closedBall_inter_ball, Set.Nonempty.mono, Set.Subset.rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ Eq.{u + 1} (α := Set α) (⋃ (n : ℕ), closedBall x (↑n : ℝ)) univ

Tactic:
iUnion_eq_univ_iff.2 fun y => exists_nat_ge (dist y x)

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, exists_nat_ge, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
rw : s ∩ ⋃ (i : ℕ), closedBall x (↑i : ℝ) = s
rw₁ : s ∩ univ = s
rw₂ rw₃ : s = s
⊢ ⋃ (n : ℕ), s ∩ closedBall x (↑n : ℝ) = s

Tactic:
rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]

Premises used: Set.inter_univ, Set.inter_iUnion, Metric.iUnion_closedBall_nat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
rw : z ∈ ball y (ε₁ + (ε₂ - ε₁))
⊢ z ∈ ball y ε₂

Tactic:
rw [← add_sub_cancel ε₁ ε₂]

Premises used: add_sub_cancel
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))

Tactic:
lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

Premises used: dist_triangle, lt_of_le_of_lt, Set.Mem, setOf, Metric.ball, add_lt_add_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y (ε₁ + (ε₂ - ε₁))

Tactic:
exact lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

Premises used: dist_triangle, lt_of_le_of_lt, add_lt_add_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
rw : dist y x ≤ ε / 2
⊢ dist y x ≤ ε - ε / 2

Tactic:
rw [sub_self_div_two]

Premises used: sub_self_div_two
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Tactic:
le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Tactic:
exact le_of_lt h

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
rw rw₁ : dist y x ≤ dist y x
⊢ dist y x ≤ ε - (ε - dist y x)

Tactic:
rw [sub_sub_self]

Premises used: sub_sub_self
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
⊢ ∃ R ≥ dist y x, ∀ z ∈ closedBall x R, p z

Tactic:
frequently_iff.1 H (Ici_mem_atTop (dist y x))

Premises used: Filter.frequently_iff, Set.Mem, Filter.Ici_mem_atTop, Iff.mp, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
obtain : ∀ (R : ℝ) (hR : R ≥ dist y x) (h : ∀ z ∈ closedBall x R, p z), p y
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
    frequently_iff.1 H (Ici_mem_atTop (dist y x))

Premises used: Filter.frequently_iff, Filter.Ici_mem_atTop, Iff.mp, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ z ∈ closedBall x R, p z
⊢ p y

Tactic:
h _ hR
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ z ∈ closedBall x R, p z
⊢ p y

Tactic:
exact h _ hR
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ ∃ R > dist y x, ∀ z ∈ ball x R, p z

Tactic:
frequently_iff.1 H (Ioi_mem_atTop (dist y x))

Premises used: Filter.frequently_iff, Set.Mem, Filter.Ioi_mem_atTop, Iff.mp, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
obtain : ∀ (R : ℝ) (hR : R > dist y x) (h : ∀ z ∈ ball x R, p z), p y
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))

Premises used: Filter.frequently_iff, Filter.Ioi_mem_atTop, Iff.mp, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
R : ℝ
hR : R > dist y x
h : ∀ z ∈ ball x R, p z
⊢ p y

Tactic:
h _ hR
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
R : ℝ
hR : R > dist y x
h : ∀ z ∈ ball x R, p z
⊢ p y

Tactic:
exact h _ hR
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₁ : sᶜ ∈ (cobounded α).sets ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₂ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ ↔
    ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₃ : (∃ (C : ℝ), ∀ x ∈ sᶜᶜ, ∀ y ∈ sᶜᶜ, dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₄ rw₅ : (∃ (C : ℝ), ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Tactic:
rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]

Premises used: Filter.mem_sets, compl_compl, Bornology.isBounded_def, Set.mem_setOf_eq, PseudoMetricSpace.cobounded_sets
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
rw :
  (∃ (C : ℝ),
      ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → dist x y ≤ C) ↔
    ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C
⊢ BoundedSpace α ↔ ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C

Tactic:
rw [← isBounded_univ, Metric.isBounded_iff]

Premises used: Metric.isBounded_iff, Bornology.isBounded_univ
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (∃ (C : ℝ),
      ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → dist x y ≤ C) ↔
    ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Tactic:
isBounded_iff.trans
    ⟨fun ⟨C, h⟩ => eventually_atTop.2 ⟨C, fun _C' hC' _x hx _y hy => (h hx hy).trans hC'⟩,
      Eventually.exists⟩

Premises used: Iff.mpr, Filter.Eventually, Metric.isBounded_iff, _private.0.Metric.isBounded_iff_eventually.match_1, Filter.Eventually.exists, Filter.atTop, Iff.intro, Exists.intro, Iff.trans, LE.le.trans, Filter.eventually_atTop
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : ℝ
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

Tactic:
⟨fun h => ((eventually_ge_atTop c).and (isBounded_iff_eventually.1 h)).exists, fun h =>
    isBounded_iff.2 <| h.imp fun _ => And.right⟩

Premises used: Iff.mpr, Metric.isBounded_iff_eventually, Filter.Eventually.and, Metric.isBounded_iff, Exists.imp, Filter.Eventually.exists, And.right, Iff.intro, Iff.mp, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ≥0), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C

Tactic:
simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
    NNReal.coe_mk, exists_prop]

Premises used: NNReal.coe_mk, dist_nndist, exists_prop, Metric.isBounded_iff_exists_ge, OfNat.ofNat, NNReal.exists, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
rw :
  (∃ (C : ℝ≥0),
      ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → nndist x y ≤ C) ↔
    ∃ (C : ℝ≥0), ∀ (a b : α), nndist a b ≤ C
⊢ BoundedSpace α ↔ ∃ (C : ℝ≥0), ∀ (a b : α), nndist a b ≤ C

Tactic:
rw [← isBounded_univ, Metric.isBounded_iff_nndist]

Premises used: Bornology.isBounded_univ, Metric.isBounded_iff_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (∃ (C : ℝ≥0),
      ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → nndist x y ≤ C) ↔
    ∃ (C : ℝ≥0), ∀ (a b : α), nndist a b ≤ C

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ (C : ℝ≥0), ∀ (a b : α), edist a b ≤ (↑C : ℝ≥0∞)

Tactic:
simp [Metric.boundedSpace_iff_nndist]

Premises used: Metric.boundedSpace_iff_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Eq.{u + 1} (α := UniformSpace α) PseudoMetricSpace.toUniformSpace (UniformSpace.ofDist dist ⋯ ⋯ ⋯)

Tactic:
UniformSpace.ext PseudoMetricSpace.uniformity_dist

Premises used: PseudoMetricSpace.uniformity_dist, UniformSpace.ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
rw : (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}
⊢ (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}

Tactic:
rw [toUniformSpace_eq]

Premises used: Metric.toUniformSpace_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}

Tactic:
UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Premises used: setOf, UniformSpace.hasBasis_ofFun, NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}

Tactic:
exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Premises used: UniformSpace.hasBasis_ofFun, NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
⊢ (𝓤 α).HasBasis p fun (i : β) ↦ {p : α × α | dist p.1 p.2 < f i}

Tactic:
⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩

Premises used: Filter.HasBasis.mem_iff, Metric.uniformity_basis_dist, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
refine :
  ∀ (s : Set (α × α)),
    (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
⊢ (𝓤 α).HasBasis p fun (i : β) ↦ {p : α × α | dist p.1 p.2 < f i}

Tactic:
refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
mpr : (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε), ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s

Tactic:
rcases hf ε₀ with ⟨i, hi, H⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s

Tactic:
⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩

Premises used: And.intro, Exists.intro, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x (hx : _ < _) => hε <| lt_of_lt_of_le hx H⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s

Tactic:
fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩

Premises used: setOf, Exists, HasSubset.Subset, Prod.fst, And, And.intro, LT.lt, Exists.intro, Dist.dist, OfNat.ofNat, Prod.snd, _private.0.Metric.mk_uniformity_basis.match_1
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (r : ℚ) ↦ 0 < r) fun (r : ℚ) ↦ {p : α × α | dist p.1 p.2 < (↑r : ℝ)}

Tactic:
Metric.mk_uniformity_basis (fun _ => Rat.cast_pos.2) fun _ε hε =>
    let ⟨r, hr0, hrε⟩ := exists_rat_btwn hε
    ⟨r, Rat.cast_pos.1 hr0, hrε.le⟩

Premises used: Iff.mpr, Exists, LT.lt.le, Rat.cast, LE.le, exists_rat_btwn, And, And.intro, LT.lt, Exists.intro, Iff.mp, Rat.cast_pos, OfNat.ofNat, _private.0.Metric.uniformity_basis_dist_rat.match_1, Metric.mk_uniformity_basis
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1}

Tactic:
Metric.mk_uniformity_basis (fun n _ => div_pos zero_lt_one <| Nat.cast_add_one_pos n) fun _ε ε0 =>
    (exists_nat_one_div_lt ε0).imp fun _n hn => ⟨trivial, le_of_lt hn⟩

Premises used: exists_nat_one_div_lt, trivial, Nat.cast_add_one_pos, le_of_lt, Exists.imp, zero_lt_one, And.intro, div_pos, Metric.mk_uniformity_basis
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (n : ℕ) ↦ 0 < n) fun (n : ℕ) ↦ {p : α × α | dist p.1 p.2 < HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)}

Tactic:
Metric.mk_uniformity_basis (fun _ hn => div_pos zero_lt_one <| Nat.cast_pos.2 hn) fun _ ε0 =>
    let ⟨n, hn⟩ := exists_nat_one_div_lt ε0
    ⟨n + 1, Nat.succ_pos n, mod_cast hn.le⟩

Premises used: Iff.mpr, exists_nat_one_div_lt, Nat.cast_pos, congrArg, Nat.cast_add._simp_1, cast, Exists, HDiv.hDiv, LT.lt.le, LE.le, Nat.cast, zero_lt_one, And, HAdd.hAdd, Nat.succ_pos, And.intro, congr, LT.lt, Exists.intro, _private.0.Metric.uniformity_basis_dist_inv_nat_pos.match_1, congrFun', div_pos, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans, Metric.mk_uniformity_basis
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
r : ℝ
h0 : 0 < r
h1 : r < 1
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | dist p.1 p.2 < r ^ n}

Tactic:
Metric.mk_uniformity_basis (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

Premises used: pow_pos, trivial, Exists, exists_pow_lt_of_lt_one, LT.lt.le, _private.0.Metric.uniformity_basis_dist_pow.match_1, LE.le, And, HPow.hPow, And.intro, True, Exists.intro, Metric.mk_uniformity_basis
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
R : ℝ
hR : 0 < R
⊢ (𝓤 α).HasBasis (fun (r : ℝ) ↦ 0 < r ∧ r < R) fun (r : ℝ) ↦ {p : α × α | dist p.1 p.2 < r}

Tactic:
Metric.mk_uniformity_basis (fun _ => And.left) fun r hr =>
    ⟨min r (R / 2), ⟨lt_min hr (half_pos hR), min_lt_iff.2 <| Or.inr (half_lt_self hR)⟩,
      min_le_left _ _⟩

Premises used: half_lt_self, Iff.mpr, half_pos, min_lt_iff, lt_min, HDiv.hDiv, min_le_left, And.left, And.intro, Exists.intro, OfNat.ofNat, Min.min, Or.inr, Metric.mk_uniformity_basis
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | dist p.1 p.2 ≤ f x}

Tactic:
⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩

Premises used: Filter.HasBasis.mem_iff, Metric.uniformity_basis_dist, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
refine :
  ∀ (s : Set (α × α)),
    (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | dist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
mpr : (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
mp : ∀ (ε' : ℝ) (hε' : 0 < ε' ∧ ε' < ε), ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases exists_between ε₀ with ⟨ε', hε'⟩

Premises used: exists_between
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε'), ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases hf ε' hε'.1 with ⟨i, hi, H⟩

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩

Premises used: lt_of_le_of_lt, And.right, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s

Tactic:
fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_setOf.2 hx.le)⟩

Premises used: Iff.mpr, setOf, Exists, LT.lt.le, HasSubset.Subset, Set.mem_setOf, Prod.fst, And, And.intro, LT.lt, Exists.intro, Dist.dist, OfNat.ofNat, Prod.snd, _private.0.Metric.mk_uniformity_basis_le.match_1
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_setOf.2 hx.le)⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (x : ℝ) ↦ 0 < x) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 ≤ ε}

Tactic:
Metric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩

Premises used: le_refl, id, Metric.mk_uniformity_basis_le, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | dist p.1 p.2 ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1}

Tactic:
Metric.mk_uniformity_basis_le (fun n _ => div_pos zero_lt_one <| Nat.cast_add_one_pos n)
    fun _ε ε0 => (exists_nat_one_div_lt ε0).imp fun _n hn => ⟨trivial, hn.le⟩

Premises used: exists_nat_one_div_lt, trivial, Nat.cast_add_one_pos, Exists.imp, Metric.mk_uniformity_basis_le, zero_lt_one, And.intro, div_pos