awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : x ∈ thickening δ E
⊢ infEDist x E < ENNReal.ofReal δ

Tactic:
rw [thickening, mem_setOf_eq] at hx

Premises used: Set.mem_setOf_eq, Metric.thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : infEDist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
hx.le

Premises used: Set.Mem, setOf, LT.lt.le, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : infEDist x E < ENNReal.ofReal δ
⊢ x ∈ cthickening δ E

Tactic:
exact hx.le

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

Tactic:
(thickening_subset_cthickening δ₁ E).trans (cthickening_mono hle E)

Premises used: Metric.cthickening_mono, Metric.thickening_subset_cthickening, HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (thickening (max (δ + 1) 1) E)

Tactic:
have : IsBounded (thickening (max (δ + 1) 1) E) := h.thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
apply : Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
⊢ Bornology.IsBounded (Metric.cthickening δ E)

Tactic:
apply this.subset

Premises used: Bornology.IsBounded.subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
⊢ cthickening δ E ⊆ thickening (max (δ + 1) 1) E

Tactic:
cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _))
    ((lt_add_one _).trans_le (le_max_left _ _)) _

Premises used: le_max_right, lt_add_one, Metric.cthickening_subset_thickening', zero_lt_one, LT.lt.trans_le, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
⊢ Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E

Tactic:
exact cthickening_subset_thickening' (zero_lt_one.trans_le (le_max_right _ _))
    ((lt_add_one _).trans_le (le_max_left _ _)) _

Premises used: le_max_right, lt_add_one, Metric.cthickening_subset_thickening', zero_lt_one, LT.lt.trans_le, le_max_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
s : Set α
hs : IsCompact s
r : ℝ
⊢ IsCompact (cthickening r s)

Tactic:
isCompact_of_isClosed_isBounded isClosed_cthickening hs.isBounded.cthickening

Premises used: IsCompact.isBounded, Metric.isCompact_of_isClosed_isBounded, Metric.isClosed_cthickening, Bornology.IsBounded.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ E ⊆ interior (cthickening δ E)

Tactic:
(subset_interior_iff_isOpen.mpr isOpen_thickening).trans
    (interior_mono (thickening_subset_cthickening δ E))

Premises used: subset_interior_iff_isOpen, Iff.mpr, Metric.thickening_subset_cthickening, interior_mono, Metric.isOpen_thickening, HasSubset.Subset.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ E) ⊆ cthickening δ E

Tactic:
(closure_mono (thickening_subset_cthickening δ E)).trans isClosed_cthickening.closure_subset

Premises used: Metric.thickening_subset_cthickening, HasSubset.Subset.trans, closure_mono, IsClosed.closure_subset, Metric.isClosed_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
rw : cthickening (min δ 0) E ⊆ cthickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ cthickening δ E

Tactic:
rw [← cthickening_of_nonpos (min_le_right δ 0)]

Premises used: min_le_right, Metric.cthickening_of_nonpos, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (min δ 0) E ⊆ cthickening δ E

Tactic:
cthickening_mono (min_le_left δ 0) E

Premises used: Metric.cthickening_mono, min_le_left, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (min δ 0) E ⊆ cthickening δ E

Tactic:
exact cthickening_mono (min_le_left δ 0) E

Premises used: Metric.cthickening_mono, min_le_left, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
rw : cthickening 0 E ⊆ thickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ thickening δ E

Tactic:
rw [← cthickening_zero]

Premises used: Metric.cthickening_zero
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E

Tactic:
cthickening_subset_thickening' δ_pos δ_pos E

Premises used: Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ cthickening 0 E ⊆ thickening δ E

Tactic:
exact cthickening_subset_thickening' δ_pos δ_pos E

Premises used: Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ E ⊆ thickening δ E

Tactic:
(@subset_closure _ _ E).trans (closure_subset_thickening δ_pos E)

Premises used: subset_closure, HasSubset.Subset.trans, Metric.closure_subset_thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ E ⊆ cthickening δ E

Tactic:
subset_closure.trans (closure_subset_cthickening δ E)

Premises used: subset_closure, HasSubset.Subset.trans, Metric.closure_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
δ : ℝ
hδ : 0 < δ
⊢ thickening δ E ∈ 𝓝ˢ E

Tactic:
isOpen_thickening.mem_nhdsSet.2 <| self_subset_thickening hδ E

Premises used: Iff.mpr, Metric.isOpen_thickening, Metric.self_subset_thickening, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
δ : ℝ
hδ : 0 < δ
⊢ cthickening δ E ∈ 𝓝ˢ E

Tactic:
mem_of_superset (thickening_mem_nhdsSet E hδ) (thickening_subset_cthickening _ _)

Premises used: Metric.thickening_subset_cthickening, Metric.thickening_mem_nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
simp_rw₂ :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x s < ENNReal.ofReal δ ∨ infEDist x t < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t

Tactic:
simp_rw [thickening, infEDist_union, min_lt_iff, setOf_or]

Premises used: min_lt_iff, Metric.infEDist_union, Metric.thickening, Set.setOf_or
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
simp_rw₂ :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x s ≤ ENNReal.ofReal δ ∨ infEDist x t ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t

Tactic:
simp_rw [cthickening, infEDist_union, min_le_iff, setOf_or]

Premises used: min_le_iff, Metric.infEDist_union, Set.setOf_or, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ι : Sort u_1
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
f : ι → Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (⋃ (i : ι), f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | ⨅ (i : ι), infEDist x (f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
simp_rw₂ :
  Eq.{u + 1} (α := Set α) {x : α | ∃ (i : ι), infEDist x (f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
⊢ Eq.{u + 1} (α := Set α) (thickening δ (⋃ (i : ι), f i)) (⋃ (i : ι), thickening δ (f i))

Tactic:
simp_rw [thickening, infEDist_iUnion, iInf_lt_iff, setOf_exists]

Premises used: Set.setOf_exists, Metric.thickening, iInf_lt_iff, Metric.infEDist_iUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ι : Type u_2
δ : ℝ
f : ι → Set α
I : Set ι
⊢ Eq.{u + 1} (α := Set α) (thickening δ (⋃ i ∈ I, f i)) (⋃ i ∈ I, thickening δ (f i))

Tactic:
simp only [thickening_iUnion]

Premises used: Metric.thickening_iUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam (cthickening (↑ε : ℝ) s) ≤ ediam s + 2 * (↑ε : ℝ≥0∞)

Tactic:
ediam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => ?_

Premises used: Metric.ediam_le, ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
refine :
  ∀ (x : α) (hx : x ∈ cthickening (↑ε : ℝ) s) (y : α) (hy : y ∈ cthickening (↑ε : ℝ) s) (δ : ℝ≥0) (hδ : 0 < δ),
    ediam s + 2 * (↑ε : ℝ≥0∞) < ∞ → edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ ediam (cthickening (↑ε : ℝ) s) ≤ ediam s + 2 * (↑ε : ℝ≥0∞)

Tactic:
refine ediam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => ?_

Premises used: Metric.ediam_le, ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε : ℝ) s
y : α
hy : y ∈ cthickening (↑ε : ℝ) s
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
rw :
  ∀ (hx : infEDist x s ≤ (↑ε : ℝ≥0∞)) (y : α) (hy : infEDist y s ≤ (↑ε : ℝ≥0∞)) (δ : ℝ≥0) (hδ : 0 < δ),
    ediam s + 2 * (↑ε : ℝ≥0∞) < ∞ → edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy

Premises used: Metric.mem_cthickening_iff, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ (↑ε : ℝ≥0∞)
y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
⊢ (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ (↑ε : ℝ≥0∞)
y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
replace hx := hx.trans_lt hε
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
obtain :
  ∀ (x' : α) (hx' : x' ∈ s) (hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)),
    edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
obtain ⟨x', hx', hxx'⟩ := infEDist_lt_iff.mp hx

Premises used: Iff.mp, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ edist x x' + edist y x'

Tactic:
edist_triangle_right _ _ _

Premises used: edist_triangle_right
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x x' + edist y x' ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s)

Tactic:
add_le_add hxx'.le (edist_le_infEDist_add_ediam hx')

Premises used: add_le_add, LT.lt.le, Metric.edist_le_infEDist_add_ediam
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
grw grw₁ : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
⊢ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)

Tactic:
grw [hy]
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
rw : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + ((↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)) + (↑δ : ℝ≥0∞)
⊢ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
rw [two_mul]

Premises used: two_mul
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + ((↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)) + (↑δ : ℝ≥0∞)

Tactic:
ac_rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : EDist.edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
edist : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
edist₁ : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ EDist.edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
calc
    edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
    _ ≤ ε + δ + (infEDist y s + ediam s) :=
      add_le_add hxx'.le (edist_le_infEDist_add_ediam hx')
    _ ≤ ε + δ + (ε + ediam s) := by grw [hy]
    _ = _ := by rw [two_mul]; ac_rfl

Premises used: ENNReal.ofNNReal, add_le_add, LT.lt.le, Metric.infEDist, edist_triangle_right, Metric.edist_le_infEDist_add_ediam, Metric.ediam, HAdd.hAdd, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam (thickening (↑ε : ℝ) s) ≤ ediam s + 2 * (↑ε : ℝ≥0∞)

Tactic:
(ediam_mono <| thickening_subset_cthickening _ _).trans <| ediam_cthickening_le _

Premises used: Metric.thickening_subset_cthickening, Metric.ediam_cthickening_le, Metric.ediam_mono, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ 0 ≤ ε

Tactic:
hε
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
lift : ∀ (ε : ℝ≥0), diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)
⊢ diam (cthickening ε s) ≤ diam s + 2 * ε

Tactic:
lift ε to ℝ≥0 using hε
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)

Tactic:
(toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_

Premises used: LE.le.trans_eq, Metric.ediam_cthickening_le, Metric.diam, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
refine_1 : ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
refine_2 : 2 * (↑ε : ℝ≥0∞) = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
refine_3 : (ediam s).toReal + (2 * (↑ε : ℝ≥0∞)).toReal = diam s + 2 * (↑ε : ℝ)
⊢ diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)

Tactic:
refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_

Premises used: LE.le.trans_eq, Metric.ediam_cthickening_le, ENNReal.toReal_le_add'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞

Tactic:
fun h ↦ top_unique <| h ▸ ediam_mono (self_subset_cthickening _)

Premises used: Eq.rec, Metric.ediam_mono, Metric.self_subset_cthickening, top_unique
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞

Tactic:
exact fun h ↦ top_unique <| h ▸ ediam_mono (self_subset_cthickening _)

Premises used: top_unique
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * (↑ε : ℝ≥0∞) = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞

Tactic:
simp [mul_eq_top]

Premises used: ENNReal.mul_eq_top
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ (ediam s).toReal + (2 * (↑ε : ℝ≥0∞)).toReal = diam s + 2 * (↑ε : ℝ)

Tactic:
simp [diam]

Premises used: Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
pos : ∀ (hs : Bornology.IsBounded s), diam (thickening ε s) ≤ diam s + 2 * ε
neg : ∀ (hs : ¬Bornology.IsBounded s), diam (thickening ε s) ≤ diam s + 2 * ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
by_cases hs : IsBounded s

Premises used: Bornology.IsBounded
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
(diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans
      (diam_cthickening_le _ hε)

Premises used: Metric.diam_mono, Metric.thickening_subset_cthickening, LE.le.trans, Bornology.IsBounded.cthickening, Metric.diam_cthickening_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans
      (diam_cthickening_le _ hε)

Premises used: Metric.diam_mono, Metric.thickening_subset_cthickening, LE.le.trans, Bornology.IsBounded.cthickening, Metric.diam_cthickening_le
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
neg : ∀ (hε : LE.le (α := ℝ) 0 0), diam (thickening 0 s) ≤ diam s + HMul.hMul (α := ℝ) 2 0
neg₁ : ∀ (hε : 0 < ε), diam (thickening ε s) ≤ diam s + 2 * ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
obtain rfl | hε := hε.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hs : ¬Bornology.IsBounded s
hε : LE.le (α := ℝ) 0 0
⊢ diam (thickening 0 s) ≤ diam s + HMul.hMul (α := ℝ) 2 0

Tactic:
simp [thickening_of_nonpos, diam_nonneg]

Premises used: Metric.diam_nonneg, Metric.thickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε_1 : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
neg : 0 ≤ diam s + 2 * ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

Tactic:
rw [diam_eq_zero_of_unbounded (mt (IsBounded.subset · <| self_subset_thickening hε _) hs)]

Premises used: Metric.diam_eq_zero_of_unbounded, mt, Bornology.IsBounded.subset, Metric.self_subset_thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε_1 : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ s = ∅ → thickening ε s = ∅

Tactic:
simp +contextual
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ (thickening ε s).Nonempty ↔ s.Nonempty

Tactic:
simp [nonempty_iff_ne_empty, thickening_eq_empty_iff_of_pos hε]

Premises used: Metric.thickening_eq_empty_iff_of_pos, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
inl : ∀ (hε : 0 < ε), thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
inr : ∀ (hε : ε ≤ 0), thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

Tactic:
obtain hε | hε := lt_or_ge 0 ε

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : 0 < ε
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

Tactic:
simp [thickening_eq_empty_iff_of_pos, hε]

Premises used: Metric.thickening_eq_empty_iff_of_pos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅

Tactic:
simp [hε, thickening_of_nonpos hε]

Premises used: Metric.thickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
⊢ (thickening ε s).Nonempty ↔ 0 < ε ∧ s.Nonempty

Tactic:
simp [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- 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 :
  ∀ (r : ℝ≥0) (hr : 0 < r) (h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y),
    ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)

Tactic:
obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst

Premises used: Metric.exists_pos_forall_lt_edist