refactor(topology): make two definitions irreducible from the start (#…

…6060)

src/topology/basic.lean

@@ -476,19 +476,22 @@ lemma closure_eq_self_union_frontier (s : set α) : closure s = s ∪ frontier s
 /-- A set is called a neighborhood of `a` if it contains an open set around `a`. The set of all
 neighborhoods of `a` forms a filter, the neighborhood filter at `a`, is here defined as the
 infimum over the principal filters of all open sets containing `a`. -/
-def nhds (a : α) : filter α := (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 s)
+@[irreducible] def nhds (a : α) : filter α := (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 s)
 
 localized "notation `𝓝` := nhds" in topological_space
 
-lemma nhds_def (a : α) : 𝓝 a = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 s) := rfl
+lemma nhds_def (a : α) : 𝓝 a = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 s) := by rw nhds
 
 /-- The open sets containing `a` are a basis for the neighborhood filter. See `nhds_basis_opens'`
 for a variant using open neighborhoods instead. -/
 lemma nhds_basis_opens (a : α) : (𝓝 a).has_basis (λ s : set α, a ∈ s ∧ is_open s) (λ x, x) :=
-has_basis_binfi_principal
-  (λ s ⟨has, hs⟩ t ⟨hat, ht⟩, ⟨s ∩ t, ⟨⟨has, hat⟩, is_open_inter hs ht⟩,
-    ⟨inter_subset_left _ _, inter_subset_right _ _⟩⟩)
-  ⟨univ, ⟨mem_univ a, is_open_univ⟩⟩
+begin
+  rw nhds_def,
+  exact has_basis_binfi_principal
+    (λ s ⟨has, hs⟩ t ⟨hat, ht⟩, ⟨s ∩ t, ⟨⟨has, hat⟩, is_open_inter hs ht⟩,
+      ⟨inter_subset_left _ _, inter_subset_right _ _⟩⟩)
+    ⟨univ, ⟨mem_univ a, is_open_univ⟩⟩
+end
 
 /-- A filter lies below the neighborhood filter at `a` iff it contains every open set around `a`. -/
 lemma le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : set α, a ∈ s → is_open s → s ∈ f :=
@@ -514,8 +517,6 @@ lemma map_nhds {a : α} {f : α → β} :
   map f (𝓝 a) = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, 𝓟 (image f s)) :=
 ((nhds_basis_opens a).map f).eq_binfi
 
-attribute [irreducible] nhds
-
 lemma mem_of_nhds {a : α} {s : set α} : s ∈ 𝓝 a → a ∈ s :=
 λ H, let ⟨t, ht, _, hs⟩ := mem_nhds_sets_iff.1 H in ht hs
 

src/topology/metric_space/hausdorff_distance.lean

@@ -149,13 +149,12 @@ end inf_edist --section
 
 /-- The Hausdorff edistance between two sets is the smallest `r` such that each set
 is contained in the `r`-neighborhood of the other one -/
-def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ℝ≥0∞ :=
+@[irreducible] def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ℝ≥0∞ :=
   Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t)
 
 lemma Hausdorff_edist_def {α : Type u} [emetric_space α] (s t : set α) :
-  Hausdorff_edist s t = Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) := rfl
-
-attribute [irreducible] Hausdorff_edist
+  Hausdorff_edist s t = Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) :=
+by rw Hausdorff_edist
 
 section Hausdorff_edist