awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)
inr :
  ∀ (y : α) (yE : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E)
    (hy : infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E) = dist x y),
    Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x
⊢ Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x

Tactic:
obtain ⟨y, yE, hy⟩ : ∃ y ∈ closure E, infDist x (closure E) = dist x y :=
    isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x

Premises used: closure_nonempty_iff, Iff.mpr, Metric.infDist, closure, IsClosed.exists_infDist_eq_dist, isClosed_closure
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)
y : α
yE : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hy : infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E) = dist x y
⊢ dist x y ≤ δ

Tactic:
replace hy : dist x y ≤ δ :=
    (ENNReal.ofReal_le_ofReal_iff hδ).mp
      (((congr_arg ENNReal.ofReal hy.symm).le.trans ENNReal.ofReal_toReal_le).trans hx)
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)
y : α
yE : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hy : dist x y ≤ δ
⊢ Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x

Tactic:
mem_biUnion yE hy

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)
y : α
yE : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hy : dist x y ≤ δ
⊢ Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x

Tactic:
exact mem_biUnion yE hy

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
rw :
  Eq.{u_2 + 1} (α := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ)
    (⋃ x ∈ E, closedBall x δ)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set α) (⋃ x ∈ E, closedBall x δ) (⋃ x ∈ E, closedBall x δ)
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]

Premises used: IsClosed.closure_eq, Metric.cthickening_eq_biUnion_closedBall
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ infEDist x s ≤ infEDist x (cthickening δ s) + ENNReal.ofReal δ

Tactic:
le_of_forall_gt fun r h => ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
refine : ∀ (r : ℝ≥0∞) (h : infEDist x (cthickening δ s) + ENNReal.ofReal δ < r), infEDist x s < r
⊢ infEDist x s ≤ infEDist x (cthickening δ s) + ENNReal.ofReal δ

Tactic:
refine le_of_forall_gt fun r h => ?_

Premises used: le_of_forall_gt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : infEDist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ ∃ (y : α), infEDist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ

Tactic:
simp_rw [← lt_tsub_iff_right, infEDist_lt_iff, mem_cthickening_iff] at h

Premises used: lt_tsub_iff_right, Metric.mem_cthickening_iff, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
h : ∃ (y : α), infEDist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
obtain : ∀ (y : α) (hy : infEDist y s ≤ ENNReal.ofReal δ) (hxy : edist x y < r - ENNReal.ofReal δ), infEDist x s < r
⊢ infEDist x s < r

Tactic:
obtain ⟨y, hy, hxy⟩ := h
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEDist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEDist x s < r

Tactic:
infEDist_le_edist_add_infEDist.trans_lt
    ((ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy).trans_eq
      (tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))

Premises used: ENNReal.ofReal_lt_top, tsub_add_cancel_of_le, LT.lt.le, LT.lt.trans_eq, Iff.mp, ENNReal.add_lt_add_of_lt_of_le, LE.le.trans, le_self_add, LE.le.trans_lt, LT.lt.ne, Metric.infEDist_le_edist_add_infEDist, lt_tsub_iff_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEDist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEDist x s < r

Tactic:
exact infEDist_le_edist_add_infEDist.trans_lt
    ((ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy).trans_eq
      (tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))

Premises used: ENNReal.ofReal_lt_top, tsub_add_cancel_of_le, LT.lt.le, LT.lt.trans_eq, Iff.mp, ENNReal.add_lt_add_of_lt_of_le, LE.le.trans, le_self_add, LE.le.trans_lt, LT.lt.ne, Metric.infEDist_le_edist_add_infEDist, lt_tsub_iff_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
bc : thickening δ s ⊆ cthickening δ s
⊢ infEDist x (cthickening δ s) + ENNReal.ofReal δ ≤ infEDist x (thickening δ s) + ENNReal.ofReal δ

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ thickening δ s ⊆ cthickening δ s

Tactic:
thickening_subset_cthickening ..

Premises used: Metric.thickening_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ thickening δ s ⊆ cthickening δ s

Tactic:
exact thickening_subset_cthickening ..

Premises used: Metric.thickening_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
inl : ∀ (hε : ε ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
inr : ∀ (hε : 0 ≤ ε), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

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

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hε, empty_subset]

Premises used: Metric.thickening_of_nonpos, Set.empty_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
inr : ∀ (hδ : δ ≤ 0), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
inr₁ : ∀ (hδ : 0 ≤ δ), thickening ε (thickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
obtain hδ | hδ := le_total δ 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : δ ≤ 0
⊢ thickening ε (thickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hδ, thickening_empty, empty_subset]

Premises used: Metric.thickening_empty, Metric.thickening_of_nonpos, Set.empty_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
inr :
  (∃ (z : α), (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ x ∈ thickening ε (thickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add hε hδ]

Premises used: Metric.mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ (z : α), (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
fun ⟨y, ⟨z, hz, hy⟩, hx⟩ =>
    ⟨z, hz, (edist_triangle _ _ _).trans_lt <| ENNReal.add_lt_add hx hy⟩

Premises used: ENNReal.ofReal, Membership.mem, Exists, And, HAdd.hAdd, And.intro, LT.lt, Exists.intro, EDist.edist, _private.0.Metric.thickening_thickening_subset.match_1, ENNReal.add_lt_add, LE.le.trans_lt, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε δ : ℝ
s : Set α
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : α
⊢ (∃ (z : α), (∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal δ) ∧ edist x z < ENNReal.ofReal ε) →
    ∃ z ∈ s, edist x z < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun ⟨y, ⟨z, hz, hy⟩, hx⟩ =>
    ⟨z, hz, (edist_triangle _ _ _).trans_lt <| ENNReal.add_lt_add hx hy⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
inl : ∀ (hε : ε ≤ 0), thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
inr : ∀ (hε : 0 ≤ ε), thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

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

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hε, empty_subset]

Premises used: Metric.thickening_of_nonpos, Set.empty_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
inr :
  (∃ (z : α), infEDist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s

Tactic:
simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEDist_lt_iff,
    ENNReal.ofReal_add hε hδ]

Premises used: Metric.mem_cthickening_iff, Metric.mem_thickening_iff_exists_edist_lt, ENNReal.ofReal_add, Metric.infEDist_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEDist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
infEDist_le_edist_add_infEDist.trans_lt
    (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)

Premises used: ENNReal.ofReal_lt_top, ENNReal.add_lt_add_of_lt_of_le, LE.le.trans_lt, LT.lt.ne, Metric.infEDist_le_edist_add_infEDist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEDist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEDist x s < ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact infEDist_le_edist_add_infEDist.trans_lt
    (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)

Premises used: ENNReal.ofReal_lt_top, ENNReal.add_lt_add_of_lt_of_le, LE.le.trans_lt, LT.lt.ne, Metric.infEDist_le_edist_add_infEDist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
inl : ∀ (hδ : δ ≤ 0), cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
inr : ∀ (hδ : 0 ≤ δ), cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
obtain hδ | hδ := le_total δ 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : δ ≤ 0
⊢ cthickening ε (thickening δ s) ⊆ cthickening (ε + δ) s

Tactic:
simp only [thickening_of_nonpos hδ, cthickening_empty, empty_subset]

Premises used: Metric.thickening_of_nonpos, Set.empty_subset, Metric.cthickening_empty
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
inr : infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ x ∈ cthickening ε (thickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]

Premises used: Metric.mem_cthickening_iff, ENNReal.ofReal_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
hx : infEDist x (thickening δ s) ≤ ENNReal.ofReal ε
grw grw₁ : ENNReal.ofReal ε + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
grw [hx]
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
hε : 0 ≤ ε
δ : ℝ
s : Set α
hδ : 0 ≤ δ
x : α
⊢ infEDist x (thickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun hx => infEDist_le_infEDist_thickening_add.trans (by grw [hx])

Premises used: Metric.infEDist_le_infEDist_thickening_add, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
simp_rw : infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ x ∈ cthickening ε (cthickening δ s) → x ∈ cthickening (ε + δ) s

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ]

Premises used: Metric.mem_cthickening_iff, ENNReal.ofReal_add
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
hx : infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε
grw grw₁ : ENNReal.ofReal ε + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) + ENNReal.ofReal δ ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
grw [hx]
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set α
x : α
⊢ infEDist x (cthickening δ s) ≤ ENNReal.ofReal ε → infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ

Tactic:
exact fun hx => infEDist_le_infEDist_cthickening_add.trans (by grw [hx])

Premises used: Metric.infEDist_le_infEDist_cthickening_add, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ≥0
hr : r₁ ≠ r₂
⊢ ENNReal.ofReal (↑r₁ : ℝ) ≠ ENNReal.ofReal (↑r₂ : ℝ)

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε δ : ℝ
rw : Subset (α := Set α) (thickening ε (thickening δ {x})) (thickening (ε + δ) {x})
⊢ thickening ε (ball x δ) ⊆ ball x (ε + δ)

Tactic:
rw [← thickening_singleton, ← thickening_singleton]

Premises used: Metric.thickening_singleton
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε δ : ℝ
⊢ Subset (α := Set α) (thickening ε (thickening δ {x})) (thickening (ε + δ) {x})

Tactic:
apply thickening_thickening_subset

Premises used: Metric.thickening_thickening_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
rw : (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε
⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
rw [(hasBasis_nhdsSet_thickening hs₁).tendsto_right_iff]

Premises used: Metric.hasBasis_nhdsSet_thickening, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
a : ∀ (ε : ℝ) (hε : 0 < ε), (∀ᶠ (x : β) in l, f x ∈ thickening ε s) ↔ ∀ᶠ (x : β) in l, infDist (f x) s < ε
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
congrm (∀ ε hε, ?_)
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
β : Type u_3
inst : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
ε : ℝ
hε : 0 < ε
⊢ (∀ᶠ (x : β) in l, f x ∈ thickening ε s) ↔ ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
simp [mem_thickening_iff_infDist_lt hs₂]

Premises used: Metric.mem_thickening_iff_infDist_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s t : Set α
hs : IsCompact s
rw rw₁ : (∃ (i : ℝ), 0 < i ∧ thickening i s ⊆ t) ↔ ∃ ε > 0, thickening ε s ⊆ t
⊢ t ∈ 𝓝ˢ s ↔ ∃ ε > 0, thickening ε s ⊆ t

Tactic:
rw [(hasBasis_nhdsSet_thickening hs).mem_iff]

Premises used: Filter.HasBasis.mem_iff, Metric.hasBasis_nhdsSet_thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s ⊆ s
⊢ thickening δ s = s

Tactic:
replace hs : thickening δ s = s := le_antisymm hs (self_subset_thickening hδ s)
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ IsClopen s

Tactic:
⟨?_, hs ▸ isOpen_thickening⟩

Premises used: Metric.isOpen_thickening, Eq.rec, And.intro, IsClopen
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
refine : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsClopen s

Tactic:
refine ⟨?_, hs ▸ isOpen_thickening⟩
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
rw : ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s ⊆ s
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
rw [← closure_subset_iff_isClosed, closure_eq_iInter_thickening]

Premises used: closure_subset_iff_isClosed, Metric.closure_eq_iInter_thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s ⊆ s

Tactic:
Set.iInter₂_subset δ hδ |>.trans_eq hs

Premises used: LE.le.trans_eq, Set.iInter₂_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : thickening δ s = s
⊢ ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ s ⊆ s

Tactic:
exact Set.iInter₂_subset δ hδ |>.trans_eq hs

Premises used: LE.le.trans_eq, Set.iInter₂_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
δ : ℝ
hδ : 0 < δ
hs : cthickening δ s ⊆ s
⊢ IsClopen s

Tactic:
.of_thickening_subset_self hδ <| (thickening_subset_cthickening δ s).trans hs

Premises used: Metric.thickening_subset_cthickening, HasSubset.Subset.trans, IsClopen.of_thickening_subset_self
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
he : ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U
hmono :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U
hunion :
  ∀ ⦃s t : Set α⦄,
    (∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U) →
      (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ (s ∪ t), thickening ε (f '' V) ⊆ U
hnhds : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U
⊢ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U

Tactic:
apply hK.induction_on (p := fun K ↦ ∃ ε > 0, ∃ V ∈ 𝓝ˢ K, thickening ε (f '' V) ⊆ U)

Premises used: IsCompact.induction_on
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ GT.gt (α := ℝ) 1 0

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ Membership.mem (γ := Filter α) (𝓝ˢ ∅) ∅

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ thickening 1 (f '' ∅) ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
w : ℝ
left : GT.gt (α := ℝ) 1 0
w₁ : Set α
left₁ : Membership.mem (γ := Filter α) (𝓝ˢ ∅) ∅
right : thickening 1 (f '' ∅) ⊆ U
⊢ ∃ ε > 0, ∃ (V : Set α), Membership.mem (γ := Filter α) (𝓝ˢ ∅) V ∧ thickening ε (f '' V) ⊆ U

Tactic:
use 1, by positivity, ∅, by simp, by simp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U

Tactic:
fun s t hst ⟨ε, hε, V, hV, hthickening⟩ ↦ ⟨ε, hε, V, nhdsSet_mono hst hV, hthickening⟩

Premises used: nhdsSet_mono, _private.0.IsCompact.exists_thickening_image_subset.match_1, Membership.mem, Exists, HasSubset.Subset, Metric.thickening, GT.gt, And, And.intro, Exists.intro, Set.image, OfNat.ofNat, nhdsSet
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
⊢ ∀ ⦃s t : Set α⦄,
    s ⊆ t → (∃ ε > 0, ∃ V ∈ 𝓝ˢ t, thickening ε (f '' V) ⊆ U) → ∃ ε > 0, ∃ V ∈ 𝓝ˢ s, thickening ε (f '' V) ⊆ U

Tactic:
exact fun s t hst ⟨ε, hε, V, hV, hthickening⟩ ↦ ⟨ε, hε, V, nhdsSet_mono hst hV, hthickening⟩