awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
⊢ cthickening δ E ⊆ thickening ε' E

Tactic:
have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
-- 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
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
ss : cthickening δ E ⊆ thickening ε' E
⊢ cthickening δ E ⊆ thickening ε E

Tactic:
ss.trans (thickening_mono hε'.2 E)

Premises used: HasSubset.Subset.trans, Metric.thickening_mono, And.right
-- 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
ε' : ℝ
hε' : ε' ∈ Ioc δ ε
ss : cthickening δ E ⊆ thickening ε' E
⊢ cthickening δ E ⊆ thickening ε E

Tactic:
exact ss.trans (thickening_mono hε'.2 E)

Premises used: HasSubset.Subset.trans, Metric.thickening_mono, And.right
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
refine_2 : Subset.{u} (α := Set α) (⋂ i ∈ s, thickening i E) (⋂ ε ∈ s, cthickening ε E)
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E

Tactic:
rw [cthickening_eq_iInter_cthickening' s hsδ hs E]

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

Tactic:
iInter₂_mono fun ε _ => thickening_subset_cthickening ε E

Premises used: Metric.thickening_subset_cthickening, Set.iInter₂_mono
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ Subset.{u} (α := Set α) (⋂ i ∈ s, thickening i E) (⋂ ε ∈ s, cthickening ε E)

Tactic:
exact iInter₂_mono fun ε _ => thickening_subset_cthickening ε E

Premises used: Metric.thickening_subset_cthickening, Set.iInter₂_mono
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
hs : ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : δ < ε), thickening ε E

Tactic:
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset

Premises used: Set.Ioi, Eq.subset, Metric.cthickening_eq_iInter_thickening', rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
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 α
δ : ℝ
δ_nn : 0 ≤ δ
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 α
δ : ℝ
δ_nn : 0 ≤ δ
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 α
δ : ℝ
E : Set α
δ_nn : 0 ≤ max 0 δ
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : max 0 δ < ε), thickening ε E

Tactic:
rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]

Premises used: Metric.cthickening_eq_iInter_thickening, Metric.cthickening_max_zero
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ

Tactic:
le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ 0 ≤ max 0 δ

Tactic:
exact le_max_left _ _

Premises used: le_max_left
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
pos : ∀ (hs₀ : s ⊆ Ioi 0), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
neg : ∀ (hs₀ : ¬s ⊆ Ioi 0), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
by_cases hs₀ : s ⊆ Ioi 0

Premises used: Set.Ioi, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : s ⊆ Ioi 0
pos : cthickening 0 E = ⋂ δ ∈ s, cthickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
rw [← cthickening_zero]

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

Tactic:
apply cthickening_eq_iInter_cthickening' _ hs₀ hs

Premises used: Metric.cthickening_eq_iInter_cthickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
neg :
  ∀ (δ : ℝ) (hδs : δ ∈ s) (δ_nonpos : δ ∉ Ioi 0),
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
obtain ⟨δ, hδs, δ_nonpos⟩ := not_subset.mp hs₀

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ∉ Ioi 0
⊢ δ ≤ 0

Tactic:
rw [Set.mem_Ioi, not_lt] at δ_nonpos

Premises used: Set.mem_Ioi, not_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
neg : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E
neg₁ : ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E

Tactic:
subset_iInter₂ fun ε _ => closure_subset_cthickening ε E

Premises used: Set.subset_iInter₂, Metric.closure_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E

Tactic:
exact subset_iInter₂ fun ε _ => closure_subset_cthickening ε E

Premises used: Set.subset_iInter₂, Metric.closure_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
neg : ⋂ δ ∈ s, cthickening δ E ⊆ cthickening δ E
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E

Tactic:
rw [← cthickening_of_nonpos δ_nonpos E]

Premises used: Metric.cthickening_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
δ : ℝ
hδs : δ ∈ s
δ_nonpos : δ ≤ 0
⊢ ⋂ δ ∈ s, cthickening δ E ⊆ cthickening δ E

Tactic:
biInter_subset_of_mem hδs

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

Tactic:
exact biInter_subset_of_mem hδs

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
rw : cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
rw [← cthickening_zero]

Premises used: Metric.cthickening_zero
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
cthickening_eq_iInter_cthickening E

Premises used: Metric.cthickening_eq_iInter_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E

Tactic:
exact cthickening_eq_iInter_cthickening E

Premises used: Metric.cthickening_eq_iInter_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
rw : cthickening 0 E = ⋂ δ ∈ s, thickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, thickening δ E

Tactic:
rw [← cthickening_zero]

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

Tactic:
apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs

Premises used: le_rfl, Metric.cthickening_eq_iInter_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
rw : cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E

Tactic:
rw [← cthickening_zero]

Premises used: Metric.cthickening_zero
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E

Tactic:
cthickening_eq_iInter_thickening rfl.ge E

Premises used: Eq.ge, Metric.cthickening_eq_iInter_thickening, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E

Tactic:
exact cthickening_eq_iInter_thickening rfl.ge E

Premises used: Eq.ge, Metric.cthickening_eq_iInter_thickening, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
δ : ℝ
⊢ frontier (cthickening δ E) ⊆ {x : α | infEDist x E = ENNReal.ofReal δ}

Tactic:
frontier_le_subset_eq continuous_infEDist continuous_const

Premises used: continuous_const, setOf, frontier_le_subset_eq, Metric.continuous_infEDist, Metric.cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E

Tactic:
(closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ ?_)

Premises used: HasSubset.Subset.trans, Metric.cthickening_subset_of_subset, Metric.closedBall_subset_cthickening_singleton
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
refine : {x} ⊆ E
⊢ closedBall x δ ⊆ cthickening δ E

Tactic:
refine (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ ?_)

Premises used: HasSubset.Subset.trans, Metric.cthickening_subset_of_subset, Metric.closedBall_subset_cthickening_singleton
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ {x} ⊆ E

Tactic:
simpa using hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
(cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_

Premises used: HasSubset.Subset.trans, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
refine : ∀ (x : α) (hx : x ∈ thickening δ' E), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_

Premises used: HasSubset.Subset.trans, Metric.cthickening_subset_thickening'
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
obtain : ∀ (y : α) (hy₁ : y ∈ E) (hy₂ : dist x y < δ'), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx

Premises used: Metric.mem_thickening_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
y : α
hy₁ : y ∈ E
hy₂ : dist x y < δ'
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x

Tactic:
mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩

Premises used: Iff.mpr, LT.lt.le, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
y : α
hy₁ : y ∈ E
hy₂ : dist x y < δ'
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x

Tactic:
exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
inl :
  ∀ (hE : IsCompact.{u_2} (X := α) ∅),
    Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ x), closedBall x δ)
inr : ∀ (hne : E.Nonempty), cthickening δ E = ⋃ x ∈ E, closedBall x δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
rcases eq_empty_or_nonempty E with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
hδ : 0 ≤ δ
hE : IsCompact.{u_2} (X := α) ∅
⊢ Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ x), closedBall x δ)

Tactic:
simp only [cthickening_empty, biUnion_empty]

Premises used: Set.biUnion_empty, Metric.cthickening_empty
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, Metric.closedBall_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
inr : ∀ (x : α) (hx : x ∈ cthickening δ E), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ

Tactic:
refine Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
⊢ ∃ y ∈ E, infEDist x E = edist x y

Tactic:
hE.exists_infEDist_eq_edist hne _

Premises used: IsCompact.exists_infEDist_eq_edist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
inr : ∀ (y : α) (yE : y ∈ E) (hy : infEDist x E = edist x y), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x

Tactic:
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEDist x E = edist x y := hE.exists_infEDist_eq_edist hne _

Premises used: Metric.infEDist, IsCompact.exists_infEDist_eq_edist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
⊢ edist x y ≤ ENNReal.ofReal δ

Tactic:
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ

Tactic:
rw [edist_dist] at D1

Premises used: edist_dist
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ

Tactic:
(ENNReal.ofReal_le_ofReal_iff hδ).1 D1

Premises used: ENNReal.ofReal_le_ofReal_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ

Tactic:
exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1

Premises used: ENNReal.ofReal_le_ofReal_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
⊢ dist x y ≤ δ

Tactic:
have D2 : dist x y ≤ δ := by
    rw [edist_dist] at D1
    exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
D2 : dist x y ≤ δ
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x

Tactic:
mem_biUnion yE D2

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
y : α
yE : y ∈ E
hy : infEDist x E = edist x y
D1 : edist x y ≤ ENNReal.ofReal δ
D2 : dist x y ≤ δ
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x

Tactic:
exact mem_biUnion yE D2

Premises used: Set.mem_biUnion
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
inl :
  Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅)
    (⋃ (x : α),
      ⋃ (_ : Membership.mem (γ := Set α) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) x),
        closedBall x δ)
inr :
  ∀ (hne : E.Nonempty),
    cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
rcases eq_empty_or_nonempty E with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hδ : 0 ≤ δ
⊢ Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅)
    (⋃ (x : α),
      ⋃ (_ : Membership.mem (γ := Set α) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) x),
        closedBall x δ)

Tactic:
simp only [cthickening_empty, biUnion_empty, closure_empty]

Premises used: Set.biUnion_empty, closure_empty, Metric.cthickening_empty
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
inr :
  cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) =
    ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
rw [← cthickening_closure]

Premises used: Metric.cthickening_closure
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) =
    ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset, Metric.closedBall_subset_cthickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
inr :
  ∀ (x : α) (hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)),
    Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x
⊢ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) =
    ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ

Tactic:
refine Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)

Premises used: Set.Subset.antisymm, Set.iUnion₂_subset
-- 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 ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E,
    infDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E) = dist x y

Tactic:
isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x

Premises used: closure_nonempty_iff, Iff.mpr, IsClosed.exists_infDist_eq_dist, isClosed_closure