awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ ≤ infEDist x E

Tactic:
exact (ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le

Premises used: ENNReal.ofReal_le_ofReal, LT.lt.le, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ E = (fun (x : α) ↦ infEDist x E) ⁻¹' Iio (ENNReal.ofReal δ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.thickening, Set.preimage, Set.Iio, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ E)

Tactic:
Continuous.isOpen_preimage continuous_infEDist _ isOpen_Iio

Premises used: Set.Mem, setOf, isOpen_Iio, Metric.thickening, Set.preimage, Metric.continuous_infEDist, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
⊢ Eq.{u + 1} (α := Set α) (thickening δ ∅) ∅

Tactic:
simp only [thickening, setOf_false, infEDist_empty, not_top_lt]

Premises used: not_top_lt, Metric.thickening, Set.setOf_false, Metric.infEDist_empty
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
s : Set α
⊢ thickening δ s = ∅

Tactic:
eq_empty_of_forall_notMem fun _ => ((ENNReal.ofReal_of_nonpos hδ).trans_le bot_le).not_gt

Premises used: Eq.trans_le, LE.le.not_gt, ENNReal.ofReal_of_nonpos, Set.eq_empty_of_forall_notMem, bot_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
hle : δ₁ ≤ δ₂
E : Set α
⊢ thickening δ₁ E ⊆ thickening δ₂ E

Tactic:
preimage_mono (Iio_subset_Iio (ENNReal.ofReal_le_ofReal hle))

Premises used: Set.Mem, setOf, ENNReal.ofReal_le_ofReal, Metric.thickening, Set.Iio_subset_Iio, Set.preimage_mono, Set.preimage
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E₁ E₂ : Set α
h : E₁ ⊆ E₂
⊢ thickening δ E₁ ⊆ thickening δ E₂

Tactic:
fun _ hx => lt_of_le_of_lt (infEDist_anti h) hx

Premises used: lt_of_le_of_lt, Set.Mem, setOf, Set.Subset, Metric.thickening, Metric.infEDist_anti
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, edist x z < ENNReal.ofReal δ

Tactic:
infEDist_lt_iff

Premises used: Set.Mem, setOf, Metric.thickening, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
δ : ℝ
⊢ frontier (thickening δ E) ⊆ {x : α | infEDist x E = ENNReal.ofReal δ}

Tactic:
frontier_lt_subset_eq continuous_infEDist continuous_const

Premises used: continuous_const, setOf, frontier_lt_subset_eq, Metric.thickening, Metric.continuous_infEDist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
⊢ Pairwise (α := ℝ) (Function.onFun.{1, u + 1, 1} (β := Set α) Disjoint fun (r : ℝ) ↦ frontier (thickening r A))

Tactic:
(pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_

Premises used: Iff.mpr, pairwise_disjoint_on
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
refine : ∀ (r₁ r₂ : ℝ) (hr : r₁ < r₂), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
⊢ Pairwise (α := ℝ) (Function.onFun.{1, u + 1, 1} (β := Set α) Disjoint fun (r : ℝ) ↦ frontier (thickening r A))

Tactic:
refine (pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_

Premises used: Iff.mpr, pairwise_disjoint_on
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
inl : ∀ (h₁ : r₁ ≤ 0), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
inr : ∀ (h₁ : 0 ≤ r₁), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
rcases le_total r₁ 0 with h₁ | h₁

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
simp [thickening_of_nonpos h₁]

Premises used: Metric.thickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
    (frontier_thickening_subset _)

Premises used: Iff.mpr, Set.disjoint_singleton, Metric.frontier_thickening_subset, Disjoint.mono, Disjoint.preimage, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
inr : ∀ (h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂), r₁ = r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
refine ((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
    (frontier_thickening_subset _)

Premises used: Iff.mpr, Set.disjoint_singleton, Metric.frontier_thickening_subset, Disjoint.mono, Disjoint.preimage, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂
⊢ (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal

Tactic:
apply_fun ENNReal.toReal at h

Premises used: ENNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
inr : ∀ (h : r₁ = (ENNReal.ofReal r₂).toReal), r₁ = r₂
inr₁ inr₂ inr₃ inr₄ : ∀ (h : r₁ = r₂), r₁ = r₂
⊢ r₁ = r₂

Tactic:
rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h

Premises used: LT.lt.le, ENNReal.toReal_ofReal, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
simp : ENNReal.ofReal δ ≤ infEDist x {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
simp only [thickening, mem_compl_iff, mem_setOf_eq, not_lt]

Premises used: Set.mem_setOf_eq, Metric.thickening, not_lt, Set.mem_compl_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
apply :
  ∀ (y : α) (hy : Membership.mem (γ := Set α) {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ y),
    ENNReal.ofReal δ ≤ edist x y
⊢ ENNReal.ofReal δ ≤ infEDist x {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ

Tactic:
apply le_infEDist.mpr fun y hy ↦ ?_

Premises used: Iff.mpr, Metric.le_infEDist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : Membership.mem (γ := Set α) {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ y
⊢ ENNReal.ofReal δ ≤ infEDist y E

Tactic:
simp only [mem_compl_iff, mem_setOf_eq, not_lt] at hy

Premises used: Set.mem_setOf_eq, not_lt, Set.mem_compl_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : ENNReal.ofReal δ ≤ infEDist y E
⊢ ENNReal.ofReal δ ≤ edist x y

Tactic:
simpa only [edist_comm] using le_trans hy <| Metric.infEDist_le_edist_of_mem x_in_E

Premises used: PseudoEMetricSpace.edist_comm, Metric.infEDist_le_edist_of_mem, le_trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
apply : Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ
⊢ thickening δ (thickening δ E)ᶜ ⊆ Eᶜ

Tactic:
apply compl_subset_compl.mp

Premises used: Set.compl_subset_compl, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ

Tactic:
simpa only [compl_compl] using subset_compl_thickening_compl_thickening_self δ E

Premises used: compl_compl, Metric.subset_compl_thickening_compl_thickening_self
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x : X
h : E.Nonempty
⊢ x ∈ thickening δ E ↔ infDist x E < δ

Tactic:
lt_ofReal_iff_toReal_lt (infEDist_ne_top h)

Premises used: Set.Mem, setOf, Metric.infDist, Metric.infEDist_ne_top, Metric.thickening, ENNReal.lt_ofReal_iff_toReal_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x z : X
rw : edist x z < ENNReal.ofReal δ ↔ (edist x z).toReal < δ
rw₁ rw₂ : (edist x z).toReal < δ ↔ (edist x z).toReal < δ
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ

Tactic:
rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]

Premises used: ENNReal.lt_ofReal_iff_toReal_lt, edist_ne_top, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x : X
⊢ ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ

Tactic:
have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
    rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
simp_rw : (∃ z ∈ E, edist x z < ENNReal.ofReal δ) ↔ ∃ z ∈ E, dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, key_iff]

Premises used: Metric.mem_thickening_iff_exists_edist_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
x : X
h : ∀ (x_1 : X), Membership.mem (γ := Set X) (thickening δ {x}) x_1 ↔ x_1 ∈ ball x δ
⊢ thickening δ {x} = ball x δ

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
x x_1 : X
⊢ Membership.mem (γ := Set X) (thickening δ {x}) x_1 ↔ x_1 ∈ ball x δ

Tactic:
simp [mem_thickening_iff]

Premises used: Metric.mem_thickening_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
x : X
E : Set X
hx : x ∈ E
δ : ℝ
⊢ ball x δ ⊆ thickening δ {x}

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : ∀ (x : X), x ∈ thickening δ E ↔ Membership.mem (γ := Set X) (⋃ x ∈ E, ball x δ) x
⊢ thickening δ E = ⋃ x ∈ E, ball x δ

Tactic:
ext x
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
h : x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ
⊢ x ∈ thickening δ E ↔ Membership.mem (γ := Set X) (⋃ x ∈ E, ball x δ) x

Tactic:
simp only [mem_iUnion₂, exists_prop]

Premises used: exists_prop, Set.mem_iUnion₂
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ

Tactic:
mem_thickening_iff

Premises used: Set.Mem, Metric.mem_thickening_iff, setOf, Metric.ball
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ

Tactic:
exact mem_thickening_iff

Premises used: Metric.mem_thickening_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
inl : ∀ (h : Bornology.IsBounded.{u} (α := X) ∅), Bornology.IsBounded.{u} (α := X) (thickening δ ∅)
inr : ∀ (x : X) (hx : x ∈ E), Bornology.IsBounded (thickening δ E)
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
h : Bornology.IsBounded.{u} (α := X) ∅
⊢ Bornology.IsBounded.{u} (α := X) (thickening δ ∅)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
(isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Metric.diam, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
inr : ∀ (y : X) (hy : y ∈ thickening δ E), y ∈ closedBall x (δ + diam E)
⊢ Bornology.IsBounded (thickening δ E)

Tactic:
refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Metric.diam, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ dist y x ≤ infDist y E + diam E

Tactic:
dist_le_infDist_add_diam (x := y) h hx

Premises used: Metric.dist_le_infDist_add_diam
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
grw grw₁ : δ + diam E ≤ δ + diam E
⊢ infDist y E + diam E ≤ δ + diam E

Tactic:
grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]

Premises used: Metric.mem_thickening_iff_infDist_lt, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
dist : infDist y E + diam E ≤ δ + diam E
⊢ y ∈ closedBall x (δ + diam E)

Tactic:
calc
      dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
      _ ≤ δ + diam E := by grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]

Premises used: Metric.infDist, Metric.dist_le_infDist_add_diam, Metric.diam, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ x ∈ cthickening δ s ↔ infEDist x s ≤ ENNReal.ofReal δ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
obtain : ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E), ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Tactic:
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEDist_of_notMem_closure h

Premises used: Metric.exists_real_pos_lt_infEDist_of_notMem_closure
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
h₁ : ∀ (δ : ℝ) (hδ : δ < ε), x ∉ cthickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E

Tactic:
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ

Premises used: eventually_lt_nhds
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
h₁ : ENNReal.ofReal δ < infEDist x E
⊢ x ∉ cthickening δ E

Tactic:
simp only [cthickening, mem_setOf_eq, not_le]

Premises used: not_le, Set.mem_setOf_eq, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEDist x E

Tactic:
((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt

Premises used: Iff.mpr, LT.lt.trans, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ < infEDist x E

Tactic:
exact ((ofReal_lt_ofReal_iff ε_pos).mpr hδ).trans ε_lt

Premises used: Iff.mpr, LT.lt.trans, ENNReal.ofReal_lt_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
(infEDist_le_edist_of_mem h).trans h'

Premises used: Metric.infEDist_le_edist_of_mem, Set.Mem, setOf, LE.le.trans, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
apply : edist x y ≤ ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
apply mem_cthickening_of_edist_le x y δ E h

Premises used: Metric.mem_cthickening_of_edist_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
rw : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ edist x y ≤ ENNReal.ofReal δ

Tactic:
rw [edist_dist]

Premises used: edist_dist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Tactic:
ENNReal.ofReal_le_ofReal h'

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Tactic:
exact ENNReal.ofReal_le_ofReal h'

Premises used: ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = (fun (x : α) ↦ infEDist x E) ⁻¹' Iic (ENNReal.ofReal δ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.Iic, rfl, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (cthickening δ E)

Tactic:
IsClosed.preimage continuous_infEDist isClosed_Iic

Premises used: Set.Mem, setOf, isClosed_Iic, Set.preimage, Metric.continuous_infEDist, IsClosed.preimage, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
⊢ Eq.{u + 1} (α := Set α) (cthickening δ ∅) ∅

Tactic:
simp only [cthickening, ENNReal.ofReal_ne_top, setOf_false, infEDist_empty, top_le_iff]

Premises used: Set.setOf_false, Metric.infEDist_empty, top_le_iff, ENNReal.ofReal_ne_top, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
h : ∀ (x : α), x ∈ cthickening δ E ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ cthickening δ E = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
ext x
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
x : α
⊢ x ∈ cthickening δ E ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
simp [mem_closure_iff_infEDist_zero, cthickening, ENNReal.ofReal_eq_zero.2 hδ]

Premises used: Iff.mpr, ENNReal.ofReal_eq_zero, Metric.mem_closure_iff_infEDist_zero, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
cthickening_of_nonpos le_rfl E

Premises used: le_rfl, Metric.cthickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
inl : δ ≤ 0 → cthickening (max 0 δ) E = cthickening δ E
inr : 0 ≤ δ → cthickening (max 0 δ) E = cthickening δ E
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
cases le_total δ 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
h : δ ≤ 0
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
simp [cthickening_of_nonpos, *]

Premises used: Metric.cthickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
h : 0 ≤ δ
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
simp [cthickening_of_nonpos, *]

Premises used: Metric.cthickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
hle : δ₁ ≤ δ₂
E : Set α
⊢ cthickening δ₁ E ⊆ cthickening δ₂ E

Tactic:
preimage_mono (Iic_subset_Iic.mpr (ENNReal.ofReal_le_ofReal hle))

Premises used: Iff.mpr, Set.Mem, Set.Iic_subset_Iic, setOf, ENNReal.ofReal_le_ofReal, Set.preimage_mono, Set.preimage, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
h : ∀ (y : α), Membership.mem (γ := Set α) (cthickening δ {x}) y ↔ y ∈ closedBall x δ
⊢ cthickening δ {x} = closedBall x δ

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
y : α
⊢ Membership.mem (γ := Set α) (cthickening δ {x}) y ↔ y ∈ closedBall x δ

Tactic:
simp [cthickening, edist_dist, ENNReal.ofReal_le_ofReal_iff hδ]

Premises used: ENNReal.ofReal_le_ofReal_iff, edist_dist, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
inl : ∀ (hδ : δ < 0), closedBall x δ ⊆ cthickening δ {x}
inr : ∀ (hδ : 0 ≤ δ), closedBall x δ ⊆ cthickening δ {x}
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
rcases lt_or_ge δ 0 with (hδ | hδ)

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
hδ : δ < 0
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [closedBall_eq_empty.mpr hδ, empty_subset]

Premises used: Iff.mpr, Metric.closedBall_eq_empty, Set.empty_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ closedBall x δ ⊆ cthickening δ {x}

Tactic:
simp only [cthickening_singleton x hδ, Subset.rfl]

Premises used: Metric.cthickening_singleton, Set.Subset.rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E₁ E₂ : Set α
h : E₁ ⊆ E₂
⊢ cthickening δ E₁ ⊆ cthickening δ E₂

Tactic:
fun _ hx => le_trans (infEDist_anti h) hx

Premises used: Set.Mem, setOf, Set.Subset, Metric.infEDist_anti, Metric.cthickening, le_trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ₁ : ℝ≥0
δ₂ : ℝ
hlt : (↑δ₁ : ℝ) < δ₂
E : Set α
⊢ cthickening (↑δ₁ : ℝ) E ⊆ thickening δ₂ E

Tactic:
fun _ hx =>
  hx.out.trans_lt ((ENNReal.ofReal_lt_ofReal_iff (lt_of_le_of_lt δ₁.prop hlt)).mpr hlt)

Premises used: Iff.mpr, lt_of_le_of_lt, Membership.mem.out, Set.Mem, setOf, Set.Subset, Metric.thickening, Subtype.prop, ENNReal.ofReal_lt_ofReal_iff, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₂_pos : 0 < δ₂
hlt : δ₁ < δ₂
E : Set α
⊢ cthickening δ₁ E ⊆ thickening δ₂ E

Tactic:
fun _ hx =>
  lt_of_le_of_lt hx.out ((ENNReal.ofReal_lt_ofReal_iff δ₂_pos).mpr hlt)

Premises used: Iff.mpr, lt_of_le_of_lt, Membership.mem.out, Set.Mem, setOf, Set.Subset, Metric.thickening, ENNReal.ofReal_lt_ofReal_iff