awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ edist x y ≤ (↑r : ℝ≥0∞)
have edist : (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: calc
    edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
    _ ≤ ↑(r / 2) + ↑(r / 2) := add_le_add hzx.le hzy.le
    _ = r := by rw [← ENNReal.coe_add, add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
have obtain : ∀ (δ : ℝ) (hδ : 0 < δ) (h : Disjoint (thickening δ s) (thickening δ t)),
  ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
Tactic: obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
have refine_1 : cthickening (δ / 2) s ≤ thickening δ s
Tactic: refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
refine_1 : cthickening (δ / 2) s ≤ thickening δ s
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t)
have refine_2 : cthickening (δ / 2) t ≤ thickening δ t
Tactic: refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
have rcases : ∀ (K : Set α) (K_compact : IsCompact K) (hK : s ⊆ interior K), ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
Tactic: rcases exists_compact_superset hs with ⟨K, K_compact, hK⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
have rcases : ∀ (δ : ℝ) (δpos : 0 < δ) (hδ : cthickening δ s ⊆ interior K), ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
Tactic: rcases hs.exists_cthickening_subset_open isOpen_interior hK with ⟨δ, δpos, hδ⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
inst_1 : LocallyCompactSpace α
hs : IsCompact s
K : Set α
K_compact : IsCompact K
hK : s ⊆ interior K
δ : ℝ
δpos : 0 < δ
hδ : cthickening δ s ⊆ interior K
⊢ ∃ (δ : ℝ), 0 < δ ∧ IsCompact (cthickening δ s)
have refine : IsCompact (cthickening δ s)
Tactic: refine ⟨δ, δpos, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, cthickening ε E
have h₁ : cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
h₁ : cthickening δ E ⊆ ⋂ ε ∈ s, cthickening ε E
⊢ cthickening δ E = ⋂ ε ∈ s, cthickening ε E
have h₂ : ⋂ ε ∈ s, cthickening ε E ⊆ cthickening δ E
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : Membership.mem (γ := Set α) (⋂ ε ∈ s, {x : α | infEDist x E ≤ ENNReal.ofReal ε}) x
⊢ Membership.mem (γ := Set α) {x : α | infEDist x E ≤ ENNReal.ofReal δ} x
have hx₁ : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
Tactic: simp only [mem_iInter, mem_setOf_eq] at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
⊢ infEDist x E ≤ ENNReal.ofReal δ
have h₂ : ∀ (ε : ℝ≥0), 0 < ε → ENNReal.ofReal δ < ∞ → infEDist x E ≤ ENNReal.ofReal δ + (↑ε : ℝ≥0∞)
Tactic: apply ENNReal.le_of_forall_pos_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
⊢ infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
have h₂ : ∀ (ε : ℝ) (hsε : ε ∈ s) (hε : ε ∈ Ioc δ (δ + (↑η : ℝ))), infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
Tactic: rcases hs (δ + η) (lt_add_of_pos_right _ (NNReal.coe_pos.mpr η_pos)) with ⟨ε, ⟨hsε, hε⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
⊢ infEDist x E ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
have h₂ : ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
Tactic: apply ((hx ε hsε).trans (ENNReal.ofReal_le_ofReal hε.2)).trans
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
x : α
hx : ∀ (i : ℝ) (i_1 : i ∈ s), infEDist x E ≤ ENNReal.ofReal i
η : ℝ≥0
η_pos : 0 < η
h : ENNReal.ofReal δ < ∞
ε : ℝ
hsε : ε ∈ s
hε : ε ∈ Ioc δ (δ + (↑η : ℝ))
⊢ ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + (↑η : ℝ≥0∞)
have h₂ : ENNReal.ofReal (δ + (↑η : ℝ)) ≤ ENNReal.ofReal δ + ENNReal.ofReal (↑η : ℝ)
Tactic: rw [ENNReal.coe_nnreal_eq η]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : δ < ε), cthickening ε E
have hs : ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
Tactic: apply cthickening_eq_iInter_cthickening' (Ioi δ) rfl.subset
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
have hs : ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
Tactic: simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E
have refine_1 : ∀ (ε : ℝ) (hε : ε ∈ s), cthickening δ E ⊆ thickening ε E
Tactic: refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
refine_1 : ∀ (ε : ℝ) (hε : ε ∈ s), cthickening δ E ⊆ thickening ε E
⊢ cthickening δ E = ⋂ ε ∈ s, thickening ε E
have refine_2 : ⋂ i ∈ s, thickening i E ⊆ cthickening δ E
Tactic: refine (subset_iInter₂ fun ε hε => ?_).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
ε : ℝ
hε : ε ∈ s
⊢ cthickening δ E ⊆ thickening ε E
have refine_1 : ∀ (ε' : ℝ) (hε' : ε' ∈ Ioc δ ε), cthickening δ E ⊆ thickening ε E
Tactic: obtain ⟨ε', -, hε'⟩ := hs ε (hsδ hε)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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
have ss : cthickening δ E ⊆ thickening ε' E
Tactic: have ss := cthickening_subset_thickening' (lt_of_le_of_lt δ_nn hε'.1) hε'.1 E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
s : Set ℝ
hsδ : s ⊆ Ioi δ
hs : ∀ (ε : ℝ), δ < ε → (s ∩ Ioc δ ε).Nonempty
E : Set α
⊢ ⋂ i ∈ s, thickening i E ⊆ cthickening δ E
have refine_2 : Subset.{u} (α := Set α) (⋂ i ∈ s, thickening i E) (⋂ ε ∈ s, cthickening ε E)
Tactic: rw [cthickening_eq_iInter_cthickening' s hsδ hs E]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : δ < ε), thickening ε E
have hs : ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
Tactic: apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty
have hs : ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
Tactic: simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening δ E = ⋂ (ε : ℝ), ⋂ (_ : max 0 δ < ε), thickening ε E
have δ_nn : 0 ≤ max 0 δ
Tactic: rw [← cthickening_max_zero, cthickening_eq_iInter_thickening]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have pos : ∀ (hs₀ : s ⊆ Ioi 0), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
Tactic: by_cases hs₀ : s ⊆ Ioi 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have neg : ∀ (hs₀ : ¬s ⊆ Ioi 0), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
Tactic: by_cases hs₀ : s ⊆ Ioi 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have pos : cthickening 0 E = ⋂ δ ∈ s, cthickening δ E
Tactic: rw [← cthickening_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
hs₀ : ¬s ⊆ Ioi 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have neg : ∀ (δ : ℝ) (hδs : δ ∈ s) (δ_nonpos : δ ∉ Ioi 0),
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
Tactic: obtain ⟨δ, hδs, δ_nonpos⟩ := not_subset.mp hs₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have δ_nonpos₁ : δ ≤ 0
Tactic: rw [Set.mem_Ioi, not_lt] at δ_nonpos
Cleared hypotheses: δ_nonpos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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
have neg : closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ ⋂ δ ∈ s, cthickening δ E
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, cthickening δ E
have neg₁ : ⋂ δ ∈ s, cthickening δ E ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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 ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have neg : ⋂ δ ∈ s, cthickening δ E ⊆ cthickening δ E
Tactic: rw [← cthickening_of_nonpos δ_nonpos E]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E
have rw : cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), cthickening δ E
Tactic: rw [← cthickening_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ δ ∈ s, thickening δ E
have rw : cthickening 0 E = ⋂ δ ∈ s, thickening δ E
Tactic: rw [← cthickening_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E
have rw : cthickening 0 E = ⋂ (δ : ℝ), ⋂ (_ : 0 < δ), thickening δ E
Tactic: rw [← cthickening_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
E : Set α
hx : x ∈ E
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ E
have refine : {x} ⊆ E
Tactic: refine (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'
have refine : ∀ (x : α) (hx : x ∈ thickening δ' E), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x
Tactic: refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x
have obtain : ∀ (y : α) (hy₁ : y ∈ E) (hy₂ : dist x y < δ'), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ') x
Tactic: obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
have inl : ∀ (hE : IsCompact.{u_2} (X := α) ∅),
  Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅) (⋃ (x : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ x), closedBall x δ)
Tactic: rcases eq_empty_or_nonempty E with (rfl | hne)
Cleared hypotheses: E, hE
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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 δ)
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
have inr : ∀ (hne : E.Nonempty), cthickening δ E = ⋃ x ∈ E, closedBall x δ
Tactic: rcases eq_empty_or_nonempty E with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
have inr : ∀ (x : α) (hx : x ∈ cthickening δ E), Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
Tactic: refine Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
hE : IsCompact E
hδ : 0 ≤ δ
hne : E.Nonempty
x : α
hx : x ∈ cthickening δ E
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
have inr : ∀ (y : α) (yE : y ∈ E) (hy : infEDist x E = edist x y), 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 _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
have D1 : edist x y ≤ ENNReal.ofReal δ
Tactic: have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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 ≤ δ
have D1₁ : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
Tactic: rw [edist_dist] at D1
Cleared hypotheses: D1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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 δ
⊢ Membership.mem (γ := Set α) (⋃ x ∈ E, closedBall x δ) x
have D2 : dist x y ≤ δ
Tactic: have D2 : dist x y ≤ δ := by
    rw [edist_dist] at D1
    exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
have inl : Eq.{u_2 + 1} (α := Set α) (cthickening δ ∅)
  (⋃ (x : α),
    ⋃ (_ : Membership.mem (γ := Set α) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) x),
      closedBall x δ)
Tactic: rcases eq_empty_or_nonempty E with (rfl | hne)
Cleared hypotheses: E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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 δ)
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
have inr : ∀ (hne : E.Nonempty),
  cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
Tactic: rcases eq_empty_or_nonempty E with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hδ : 0 ≤ δ
hne : E.Nonempty
⊢ cthickening δ E = ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
have inr : cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) =
  ⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ
Tactic: rw [← cthickening_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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 δ
have inr : ∀ (x : α) (hx : x ∈ cthickening δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E)),
  Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x
Tactic: refine Subset.antisymm (fun x hx ↦ ?_)
    (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
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)
⊢ Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x
have 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
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
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
⊢ Membership.mem (γ := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ) x
have hy₁ : 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)
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
E : Set α
hE : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ x ∈ E, closedBall x δ
have rw : Eq.{u_2 + 1} (α := Set α) (⋃ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] E, closedBall x δ)
  (⋃ x ∈ E, closedBall x δ)
Tactic: rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]