awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩

Premises used: Iff.mpr, half_pos, HDiv.hDiv, And.intro, Exists.intro, NNReal.coe_pos, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
refine : Disjoint (thickening ((↑r : ℝ) / 2) s) (thickening ((↑r : ℝ) / 2) t)
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
refine ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
rw : thickening ((↑r : ℝ) / 2) s ⊓ thickening ((↑r : ℝ) / 2) t ≤ ⊥
⊢ Disjoint (thickening ((↑r : ℝ) / 2) s) (thickening ((↑r : ℝ) / 2) t)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : z ∈ thickening ((↑r : ℝ) / 2) s
hzt : z ∈ thickening ((↑r : ℝ) / 2) t
⊢ ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)

Tactic:
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt

Premises used: Metric.mem_thickening_iff_exists_edist_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : z ∈ thickening ((↑r : ℝ) / 2) s
hzt : z ∈ thickening ((↑r : ℝ) / 2) t
hzs₁ : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
⊢ ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)

Tactic:
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt

Premises used: Metric.mem_thickening_iff_exists_edist_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
⊢ ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)

Tactic:
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt

Premises used: NNReal.coe_div, NNReal.coe_two, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzs₁ : ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
⊢ ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)

Tactic:
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt

Premises used: NNReal.coe_div, NNReal.coe_two, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
hzt : ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
obtain : ∀ (x : α) (hx : x ∈ s) (hzx : edist z x < (↑(r / 2) : ℝ≥0∞)), Membership.mem (γ := Set α) ⊥ z
⊢ Membership.mem (γ := Set α) ⊥ z

Tactic:
obtain ⟨x, hx, hzx⟩ := hzs
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzt : ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
obtain : ∀ (y : α) (hy : y ∈ t) (hzy : edist z y < (↑(r / 2) : ℝ≥0∞)), Membership.mem (γ := Set α) ⊥ z
⊢ Membership.mem (γ := Set α) ⊥ z

Tactic:
obtain ⟨y, hy, hzy⟩ := hzt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z

Tactic:
(h x hx y hy).not_ge ?_

Premises used: Set.Mem, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
refine : edist x y ≤ (↑r : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z

Tactic:
refine (h x hx y hy).not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ edist x y ≤ edist z x + edist z y

Tactic:
edist_triangle_left _ _ _

Premises used: edist_triangle_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ edist z x + edist z y ≤ (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞)

Tactic:
add_le_add hzx.le hzy.le

Premises used: add_le_add, LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
rw : (↑(r / 2 + r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
rw₁ rw₂ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)

Tactic:
rw [← ENNReal.coe_add, add_halves]

Premises used: add_halves, ENNReal.coe_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < EDist.edist x y
z x : α
hx : x ∈ s
hzx : EDist.edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : EDist.edist z y < (↑(r / 2) : ℝ≥0∞)
edist : (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ EDist.edist x y ≤ (↑r : ℝ≥0∞)

Tactic:
calc
    edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
    _ ≤ ↑(r / 2) + ↑(r / 2) := add_le_add hzx.le hzy.le
    _ = r := by rw [← ENNReal.coe_add, add_halves]

Premises used: add_le_add, HDiv.hDiv, LT.lt.le, EDist.edist, edist_triangle_left, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
obtain :
  ∀ (δ : ℝ) (hδ : 0 < δ) (h : Disjoint (thickening δ s) (thickening δ t)),
    ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht

Premises used: Disjoint.exists_thickenings
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩

Premises used: half_pos, HDiv.hDiv, And.intro, Exists.intro, Disjoint.mono, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
refine_1 : cthickening (δ / 2) s ≤ thickening δ s
refine_2 : cthickening (δ / 2) t ≤ thickening δ t
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)

Tactic:
refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ≤ thickening δ s

Tactic:
cthickening_subset_thickening' hδ (half_lt_self hδ) _

Premises used: half_lt_self, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ≤ thickening δ s

Tactic:
exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

Premises used: half_lt_self, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ≤ thickening δ t

Tactic:
cthickening_subset_thickening' hδ (half_lt_self hδ) _

Premises used: half_lt_self, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ≤ thickening δ t

Tactic:
exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

Premises used: half_lt_self, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : s ⊆ t
⊢ ∃ (δ : ℝ), 0 < δ ∧ cthickening δ s ⊆ t

Tactic:
(hst.disjoint_compl_right.exists_cthickenings hs ht.isClosed_compl).imp fun _ h =>
    ⟨h.1, disjoint_compl_right_iff_subset.1 <| h.2.mono_right <| self_subset_cthickening _⟩

Premises used: Disjoint.exists_cthickenings, HasSubset.Subset.disjoint_compl_right, Exists.imp, Set.disjoint_compl_right_iff_subset, IsOpen.isClosed_compl, And.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
rcases : ∀ (K : Set α) (K_compact : IsCompact K) (hK : s ⊆ interior K), ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩

Premises used: exists_compact_superset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
rcases : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : cthickening δ s ⊆ interior K), ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩

Premises used: isOpen_interior, IsCompact.exists_cthickening_subset_open
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
⟨δ, δpos, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
refine : IsCompact (cthickening δ s)
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)

Tactic:
refine ⟨δ, δpos, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ IsCompact (cthickening δ s)

Tactic:
K_compact.of_isClosed_subset isClosed_cthickening (hδ.trans interior_subset)

Premises used: interior_subset, HasSubset.Subset.trans, IsCompact.of_isClosed_subset, Metric.isClosed_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ IsCompact (cthickening δ s)

Tactic:
exact K_compact.of_isClosed_subset isClosed_cthickening (hδ.trans interior_subset)

Premises used: interior_subset, HasSubset.Subset.trans, IsCompact.of_isClosed_subset, Metric.isClosed_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hs : IsCompact s
ht : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hst : s ⊆ t
⊢ ∃ (δ : ℝ), 0 < δ ∧ thickening δ s ⊆ t

Tactic:
let ⟨δ, h₀, hδ⟩ := hs.exists_cthickening_subset_open ht hst
  ⟨δ, h₀, (thickening_subset_cthickening _ _).trans hδ⟩

Premises used: Metric.thickening_subset_cthickening, Exists, HasSubset.Subset.trans, HasSubset.Subset, Metric.thickening, And, And.intro, LT.lt, _private.0.IsCompact.exists_thickening_subset_open.match_1, IsCompact.exists_cthickening_subset_open, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : Set α
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun (δ : ℝ) ↦ 0 < δ) fun (δ : ℝ) ↦ thickening δ K

Tactic:
(hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_thickening_subset_open hU.1 hU.2)
    fun _ => thickening_mem_nhdsSet K

Premises used: hasBasis_nhdsSet, And.right, And.left, Filter.HasBasis.to_hasBasis', IsCompact.exists_thickening_subset_open, Metric.thickening_mem_nhdsSet
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : Set α
hK : IsCompact K
⊢ (𝓝ˢ K).HasBasis (fun (δ : ℝ) ↦ 0 < δ) fun (δ : ℝ) ↦ cthickening δ K

Tactic:
(hasBasis_nhdsSet K).to_hasBasis' (fun _U hU => hK.exists_cthickening_subset_open hU.1 hU.2)
    fun _ => cthickening_mem_nhdsSet K

Premises used: hasBasis_nhdsSet, Metric.cthickening_mem_nhdsSet, And.right, And.left, IsCompact.exists_cthickening_subset_open, Filter.HasBasis.to_hasBasis'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
h₁ : cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E
h₂ : ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E
⊢ cthickening δ E = ⋂ ε ∈ s, cthickening ε E

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

Tactic:
subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E

Premises used: Metric.cthickening_mono, le_of_lt, Set.subset_iInter₂
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E

Tactic:
exact subset_iInter₂ fun _ hε => cthickening_mono (le_of_lt (hsδ hε)) E

Premises used: Metric.cthickening_mono, le_of_lt, Set.subset_iInter₂
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : Membership.mem (γ := Set α) (⋂ ε ∈ s, {x : α | infEDist x E ≤ ENNReal.ofReal ε}) x
⊢ ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i

Tactic:
simp only [mem_iInter, mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
h₂ : ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + (↑ε : ℝ≥0∞)
⊢ infEDist x E ≤ ENNReal.ofReal δ

Tactic:
apply ENNReal.le_of_forall_pos_le_add

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h₂ : ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
⊢ ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
h₂ : ∀ (ε : ℝ) (hsε : ε ∈ s) (hε : ε ∈ Ioc δ (δ + (↑η : ℝ))), infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
⊢ infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)

Tactic:
rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩

Premises used: Iff.mpr, lt_add_of_pos_right, HAdd.hAdd, NNReal.coe_pos, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
h₂ : ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
⊢ infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)

Tactic:
apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans

Premises used: ENNReal.ofReal_le_ofReal, And.right, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
h₂ : ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + ENNReal.ofReal (↑η : ℝ)
⊢ ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_nnreal_eq η]

Premises used: ENNReal.coe_nnreal_eq
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
⊢ ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + ENNReal.ofReal (↑η : ℝ)

Tactic:
ENNReal.ofReal_add_le

Premises used: ENNReal.ofReal_add_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
⊢ ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + ENNReal.ofReal (↑η : ℝ)

Tactic:
exact ENNReal.ofReal_add_le

Premises used: ENNReal.ofReal_add_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
hs : ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : δ < ε), cthickening ε E

Tactic:
apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset

Premises used: Set.Ioi, Metric.cthickening_eq_iInter_cthickening', Eq.subset, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
hs : ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Tactic:
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]

Premises used: Iff.mpr, Set.inter_eq_right, Set.Ioc_subset_Ioi_self
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty

Tactic:
fun _ hε => nonempty_Ioc.mpr hε

Premises used: Iff.mpr, Set.nonempty_Ioc
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty

Tactic:
exact fun _ hε => nonempty_Ioc.mpr hε

Premises used: Iff.mpr, Set.nonempty_Ioc
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E

Tactic:
(subset_iInter₂ fun ε hε => ?_).antisymm ?_

Premises used: Set.subset_iInter₂, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
refine_1 : ∀ (ε : ℝ) (hε : ε ∈ s), cthickening δ E ⊆ thickening ε E
refine_2 : ⋂ i ∈ s, thickening i E ⊆ cthickening δ E
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E

Tactic:
refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_

Premises used: Set.subset_iInter₂, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
refine_1 : ∀ (ε' : ℝ) (hε' : ε' ∈ Ioc δ ε), cthickening δ E ⊆ thickening ε E
⊢ cthickening δ E ⊆ thickening ε E

Tactic:
obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)