chore(*): restore subsingleton instances and remove hacks (#16046)

#### Background

The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so.

This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible.

Therefore, in this PR, we:

+ Remove both hacks remaining;

+ Turn all would-be instances that mention gh-6025 into actual global instances;

+ Golf proofs that explicitly invoked these instances previously;

+ Remove `local attribute [instance]` lines that were added when these instances were needed.

Closes #6025.

src/algebra/algebra/basic.lean

@@ -1337,8 +1337,7 @@ example : algebra_rat = algebra.id ℚ := rfl
 @[simp] theorem algebra_map_rat_rat : algebra_map ℚ ℚ = ring_hom.id ℚ :=
 subsingleton.elim _ _
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma algebra_rat_subsingleton {α} [semiring α] :
+instance algebra_rat_subsingleton {α} [semiring α] :
   subsingleton (algebra ℚ α) :=
 ⟨λ x y, algebra.algebra_ext x y $ ring_hom.congr_fun $ subsingleton.elim _ _⟩
 

src/algebra/algebra/subalgebra/basic.lean

@@ -701,41 +701,22 @@ This is the algebra version of `submodule.top_equiv`. -/
 @[simps] def top_equiv : (⊤ : subalgebra R A) ≃ₐ[R] A :=
 alg_equiv.of_alg_hom (subalgebra.val ⊤) to_top rfl $ alg_hom.ext $ λ _, subtype.ext rfl
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_subsingleton [subsingleton A] : subsingleton (subalgebra R A) :=
+instance subsingleton_of_subsingleton [subsingleton A] : subsingleton (subalgebra R A) :=
 ⟨λ B C, ext (λ x, by { simp only [subsingleton.elim x 0, zero_mem B, zero_mem C] })⟩
 
-/--
-For performance reasons this is not an instance. If you need this instance, add
-```
-local attribute [instance] alg_hom.subsingleton subalgebra.subsingleton_of_subsingleton
-```
-in the section that needs it.
--/
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma _root_.alg_hom.subsingleton [subsingleton (subalgebra R A)] : subsingleton (A →ₐ[R] B) :=
+instance _root_.alg_hom.subsingleton [subsingleton (subalgebra R A)] : subsingleton (A →ₐ[R] B) :=
 ⟨λ f g, alg_hom.ext $ λ a,
   have a ∈ (⊥ : subalgebra R A) := subsingleton.elim (⊤ : subalgebra R A) ⊥ ▸ mem_top,
   let ⟨x, hx⟩ := set.mem_range.mp (mem_bot.mp this) in
   hx ▸ (f.commutes _).trans (g.commutes _).symm⟩
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma _root_.alg_equiv.subsingleton_left [subsingleton (subalgebra R A)] :
+instance _root_.alg_equiv.subsingleton_left [subsingleton (subalgebra R A)] :
   subsingleton (A ≃ₐ[R] B) :=
-begin
-  haveI : subsingleton (A →ₐ[R] B) := alg_hom.subsingleton,
-  exact ⟨λ f g, alg_equiv.ext
-    (λ x, alg_hom.ext_iff.mp (subsingleton.elim f.to_alg_hom g.to_alg_hom) x)⟩,
-end
+⟨λ f g, alg_equiv.ext (λ x, alg_hom.ext_iff.mp (subsingleton.elim f.to_alg_hom g.to_alg_hom) x)⟩
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma _root_.alg_equiv.subsingleton_right [subsingleton (subalgebra R B)] :
+instance _root_.alg_equiv.subsingleton_right [subsingleton (subalgebra R B)] :
   subsingleton (A ≃ₐ[R] B) :=
-begin
-  haveI : subsingleton (B ≃ₐ[R] A) := alg_equiv.subsingleton_left,
-  exact ⟨λ f g, eq.trans (alg_equiv.symm_symm _).symm
-    (by rw [subsingleton.elim f.symm g.symm, alg_equiv.symm_symm])⟩
-end
+⟨λ f g, by rw [← f.symm_symm, subsingleton.elim f.symm g.symm, g.symm_symm]⟩
 
 lemma range_val : S.val.range = S :=
 ext $ set.ext_iff.1 $ S.val.coe_range.trans subtype.range_val

src/algebra/lie/solvable.lean

@@ -187,7 +187,7 @@ class is_solvable : Prop :=
 (solvable : ∃ k, derived_series R L k = ⊥)
 
 instance is_solvable_bot : is_solvable R ↥(⊥ : lie_ideal R L) :=
-⟨⟨0, @subsingleton.elim _ lie_ideal.subsingleton_of_bot _ ⊥⟩⟩
+⟨⟨0, subsingleton.elim _ ⊥⟩⟩
 
 instance is_solvable_add {I J : lie_ideal R L} [hI : is_solvable R I] [hJ : is_solvable R J] :
   is_solvable R ↥(I + J) :=

src/algebra/lie/subalgebra.lean

@@ -400,8 +400,7 @@ by rw [← mem_coe_submodule, ← mem_coe_submodule, ← mem_coe_submodule, inf_
 lemma eq_bot_iff : K = ⊥ ↔ ∀ (x : L), x ∈ K → x = 0 :=
 by { rw eq_bot_iff, exact iff.rfl, }
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_bot : subsingleton (lie_subalgebra R ↥(⊥ : lie_subalgebra R L)) :=
+instance subsingleton_of_bot : subsingleton (lie_subalgebra R ↥(⊥ : lie_subalgebra R L)) :=
 begin
   apply subsingleton_of_bot_eq_top,
   ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_subalgebra.mem_bot at hx, subst hx,

src/algebra/lie/submodule.lean

@@ -373,8 +373,7 @@ by { rw [← mem_coe_submodule, sup_coe_to_submodule, submodule.mem_sup], exact
 lemma eq_bot_iff : N = ⊥ ↔ ∀ (m : M), m ∈ N → m = 0 :=
 by { rw eq_bot_iff, exact iff.rfl, }
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_bot : subsingleton (lie_submodule R L ↥(⊥ : lie_submodule R L M)) :=
+instance subsingleton_of_bot : subsingleton (lie_submodule R L ↥(⊥ : lie_submodule R L M)) :=
 begin
   apply subsingleton_of_bot_eq_top,
   ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_submodule.mem_bot at hx, subst hx,
@@ -666,8 +665,7 @@ different (though the latter does naturally inject into the former).
 
 In other words, in general, ideals of `I`, regarded as a Lie algebra in its own right, are not the
 same as ideals of `L` contained in `I`. -/
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_bot : subsingleton (lie_ideal R (⊥ : lie_ideal R L)) :=
+instance subsingleton_of_bot : subsingleton (lie_ideal R (⊥ : lie_ideal R L)) :=
 begin
   apply subsingleton_of_bot_eq_top,
   ext ⟨x, hx⟩, change x ∈ ⊥ at hx, rw lie_submodule.mem_bot at hx, subst hx,

src/algebra/module/basic.lean

@@ -416,10 +416,8 @@ lemma map_rat_smul [add_comm_group M] [add_comm_group M₂] [module ℚ M] [modu
   f (c • x) = c • f x :=
 rat.cast_id c ▸ map_rat_cast_smul f ℚ ℚ c x
 
-/-- There can be at most one `module ℚ E` structure on an additive commutative group. This is not
-an instance because `simp` becomes very slow if we have many `subsingleton` instances,
-see [gh-6025]. -/
-lemma subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (module ℚ E) :=
+/-- There can be at most one `module ℚ E` structure on an additive commutative group. -/
+instance subsingleton_rat_module (E : Type*) [add_comm_group E] : subsingleton (module ℚ E) :=
 ⟨λ P Q, module.ext' P Q $ λ r x,
   @map_rat_smul _ _ _ _ P Q _ _ (add_monoid_hom.id E) r x⟩
 

src/algebra/order/complete_field.lean

@@ -300,8 +300,6 @@ order_ring_iso.ext induced_map_self
 
 open order_ring_iso
 
-local attribute [instance] order_ring_hom.subsingleton order_ring_iso.subsingleton_left
-
 /-- There is a unique ordered ring homomorphism from an archimedean linear ordered field to a
 conditionally complete linear ordered field. -/
 instance : unique (α →+*o β) := unique_of_subsingleton $ induced_order_ring_hom α β

src/algebra/order/hom/ring.lean

@@ -315,8 +315,7 @@ conditionally complete.
 
 /-- There is at most one ordered ring homomorphism from a linear ordered field to an archimedean
 linear ordered field. -/
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_field β]
+instance order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_field β]
   [archimedean β] :
   subsingleton (α →+*o β) :=
 ⟨λ f g, begin
@@ -331,22 +330,16 @@ lemma order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_fiel
     (order_hom_class.mono f).reflect_lt hf).elim,
 end⟩
 
-local attribute [instance] order_ring_hom.subsingleton
-
 /-- There is at most one ordered ring isomorphism between a linear ordered field and an archimedean
 linear ordered field. -/
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma order_ring_iso.subsingleton_right [linear_ordered_field α] [linear_ordered_field β]
+instance order_ring_iso.subsingleton_right [linear_ordered_field α] [linear_ordered_field β]
   [archimedean β] :
   subsingleton (α ≃+*o β) :=
 order_ring_iso.to_order_ring_hom_injective.subsingleton
 
-local attribute [instance] order_ring_iso.subsingleton_right
-
 /-- There is at most one ordered ring isomorphism between an archimedean linear ordered field and a
 linear ordered field. -/
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma order_ring_iso.subsingleton_left [linear_ordered_field α] [archimedean α]
+instance order_ring_iso.subsingleton_left [linear_ordered_field α] [archimedean α]
   [linear_ordered_field β] :
   subsingleton (α ≃+*o β) :=
 order_ring_iso.symm_bijective.injective.subsingleton

src/analysis/normed_space/multilinear.lean

@@ -60,9 +60,6 @@ open finset metric
 local attribute [instance, priority 1001]
 add_comm_group.to_add_comm_monoid normed_add_comm_group.to_add_comm_group normed_space.to_module'
 
--- hack to speed up simp when dealing with complicated types
-local attribute [-instance] unique.subsingleton pi.subsingleton
-
 /-!
 ### Type variables
 
@@ -1240,7 +1237,6 @@ isomorphic (and even isometric) to `E₂`. As this is the zeroth step in the con
 derivatives, we register this isomorphism. -/
 
 section
-local attribute [instance] unique.subsingleton
 
 variables {𝕜 G G'}
 

src/data/list/basic.lean

@@ -17,9 +17,8 @@ variables {ι : Type*} {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
 
 attribute [inline] list.head
 
--- TODO[gh-6025]: make this an instance once safe to do so
 /-- There is only one list of an empty type -/
-def unique_of_is_empty [is_empty α] : unique (list α) :=
+instance unique_of_is_empty [is_empty α] : unique (list α) :=
 { uniq := λ l, match l with
     | [] := rfl
     | (a :: l) := is_empty_elim a

src/data/matrix/basic.lean

@@ -213,12 +213,10 @@ lemma _root_.is_left_regular.matrix [has_mul α] {k : α} (hk : is_left_regular
   is_smul_regular (matrix m n α) k :=
 hk.is_smul_regular.matrix
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) :=
+instance subsingleton_of_empty_left [is_empty m] : subsingleton (matrix m n α) :=
 ⟨λ M N, by { ext, exact is_empty_elim i }⟩
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) :=
+instance subsingleton_of_empty_right [is_empty n] : subsingleton (matrix m n α) :=
 ⟨λ M N, by { ext, exact is_empty_elim j }⟩
 
 end matrix

src/data/matrix/dmatrix.lean

@@ -104,12 +104,10 @@ lemma map_sub [∀ i j, add_group (α i j)] {β : m → n → Type w} [∀ i j,
   (M - N).map (λ i j, @f i j) = M.map (λ i j, @f i j) - N.map (λ i j, @f i j) :=
 by { ext, simp }
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_empty_left [is_empty m] : subsingleton (dmatrix m n α) :=
+instance subsingleton_of_empty_left [is_empty m] : subsingleton (dmatrix m n α) :=
 ⟨λ M N, by { ext, exact is_empty_elim i }⟩
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subsingleton_of_empty_right [is_empty n] : subsingleton (dmatrix m n α) :=
+instance subsingleton_of_empty_right [is_empty n] : subsingleton (dmatrix m n α) :=
 ⟨λ M N, by { ext, exact is_empty_elim j }⟩
 
 end dmatrix

src/data/mv_polynomial/basic.lean

@@ -128,9 +128,8 @@ instance is_scalar_tower' [comm_semiring R] [comm_semiring S₁] [algebra R S₁
   is_scalar_tower R (mv_polynomial σ S₁) (mv_polynomial σ S₁) :=
 is_scalar_tower.right
 
--- TODO[gh-6025]: make this an instance once safe to do so
 /-- If `R` is a subsingleton, then `mv_polynomial σ R` has a unique element -/
-protected def unique [comm_semiring R] [subsingleton R] : unique (mv_polynomial σ R) :=
+instance unique [comm_semiring R] [subsingleton R] : unique (mv_polynomial σ R) :=
 add_monoid_algebra.unique
 
 end instances

src/geometry/manifold/charted_space.lean

@@ -121,12 +121,6 @@ the arrow. -/
 localized "infixr  ` ≫ₕ `:100 := local_homeomorph.trans" in manifold
 localized "infixr  ` ≫ `:100 := local_equiv.trans" in manifold
 
-/- `simp` looks for subsingleton instances at every call. This turns out to be very
-inefficient, especially in `simp`-heavy parts of the library such as the manifold code.
-Disable two such instances to speed up things.
-NB: this is just a hack. TODO: fix `simp` properly. -/
-localized "attribute [-instance] unique.subsingleton pi.subsingleton" in manifold
-
 open set local_homeomorph
 
 /-! ### Structure groupoids-/

src/linear_algebra/matrix/adjugate.lean

@@ -336,7 +336,7 @@ begin
 end
 
 @[simp] lemma adjugate_fin_zero (A : matrix (fin 0) (fin 0) α) : adjugate A = 0 :=
-@subsingleton.elim _ matrix.subsingleton_of_empty_left _ _
+subsingleton.elim _ _
 
 @[simp] lemma adjugate_fin_one (A : matrix (fin 1) (fin 1) α) : adjugate A = 1 :=
 adjugate_subsingleton A
@@ -442,7 +442,7 @@ begin
   -- get rid of the `- 2`
   cases h_card : (fintype.card n) with n',
   { haveI : is_empty n := fintype.card_eq_zero_iff.mp h_card,
-    exact @subsingleton.elim _ (matrix.subsingleton_of_empty_left) _ _, },
+    apply subsingleton.elim, },
   cases n',
   { exact (h h_card).elim },
   rw ←h_card,

src/linear_algebra/matrix/charpoly/finite_field.lean

@@ -37,9 +37,7 @@ begin
     rw [alg_equiv.map_pow, mat_poly_equiv_charmatrix, hk, sub_pow_char_pow_of_commute, ← C_pow],
     { exact (id (mat_poly_equiv_eq_X_pow_sub_C (p ^ k) M) : _) },
     { exact (C M).commute_X } },
-  { -- TODO[gh-6025]: remove this `haveI` once `subsingleton_of_empty_right` is a global instance
-    haveI : subsingleton (matrix n n K) := subsingleton_of_empty_right,
-    exact congr_arg _ (subsingleton.elim _ _), },
+  { exact congr_arg _ (subsingleton.elim _ _), },
 end
 
 @[simp] lemma zmod.charpoly_pow_card {p : ℕ} [fact p.prime] (M : matrix n n (zmod p)) :

src/logic/basic.lean

@@ -71,8 +71,8 @@ lemma subsingleton_of_forall_eq {α : Sort*} (x : α) (h : ∀ y, y = x) : subsi
 lemma subsingleton_iff_forall_eq {α : Sort*} (x : α) : subsingleton α ↔ ∀ y, y = x :=
 ⟨λ h y, @subsingleton.elim _ h y x, subsingleton_of_forall_eq x⟩
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma subtype.subsingleton (α : Sort*) [subsingleton α] (p : α → Prop) : subsingleton (subtype p) :=
+instance subtype.subsingleton (α : Sort*) [subsingleton α] (p : α → Prop) :
+  subsingleton (subtype p) :=
 ⟨λ ⟨x,_⟩ ⟨y,_⟩, have x = y, from subsingleton.elim _ _, by { cases this, refl }⟩
 
 /-- Add an instance to "undo" coercion transitivity into a chain of coercions, because

src/number_theory/cyclotomic/basic.lean

@@ -139,9 +139,9 @@ begin
     rw [mem_singleton_iff, ←pnat.coe_eq_one_iff],
     exact_mod_cast hζ.unique (is_primitive_root.of_subsingleton ζ) },
   { rintro (rfl|rfl),
-    { refine ⟨λ _ h, h.elim, λ x, by convert subalgebra.zero_mem _⟩ },
+    { refine ⟨λ _ h, h.elim, λ x, by convert (mem_top : x ∈ ⊤)⟩ },
     { rw iff_singleton,
-      refine ⟨⟨0, is_primitive_root.of_subsingleton 0⟩, λ x, by convert subalgebra.zero_mem _⟩ } }
+      refine ⟨⟨0, is_primitive_root.of_subsingleton 0⟩, λ x, by convert (mem_top : x ∈ ⊤)⟩ } }
 end
 
 /-- If `B` is a cyclotomic extension of `A` given by roots of unity of order in `S ∪ T`, then `B`

src/number_theory/cyclotomic/rat.lean

@@ -130,7 +130,6 @@ begin
 end
 
 local attribute [-instance] cyclotomic_field.algebra
-local attribute [instance] algebra_rat_subsingleton
 
 /-- The integral closure of `ℤ` inside `cyclotomic_field (p ^ k) ℚ` is
 `cyclotomic_ring (p ^ k) ℤ ℚ`. -/

src/number_theory/number_field.lean

@@ -137,8 +137,6 @@ namespace rat
 
 open number_field
 
-local attribute [instance] subsingleton_rat_module
-
 instance number_field : number_field ℚ :=
 { to_char_zero := infer_instance,
   to_finite_dimensional :=
@@ -161,7 +159,6 @@ section
 open_locale polynomial
 
 local attribute [-instance] algebra_rat
-local attribute [instance] algebra_rat_subsingleton
 
 /-- The quotient of `ℚ[X]` by the ideal generated by an irreducible polynomial of `ℚ[X]`
 is a number field. -/

src/order/filter/basic.lean

@@ -631,9 +631,7 @@ lemma inf_eq_bot_iff {f g : filter α} :
 by simpa only [disjoint_iff] using filter.disjoint_iff
 
 /-- There is exactly one filter on an empty type. --/
--- TODO[gh-6025]: make this globally an instance once safe to do so
-local attribute [instance]
-protected def unique [is_empty α] : unique (filter α) :=
+instance unique [is_empty α] : unique (filter α) :=
 { default := ⊥, uniq := filter_eq_bot_of_is_empty }
 
 /-- There are only two filters on a `subsingleton`: `⊥` and `⊤`. If the type is empty, then they are

src/order/hom/basic.lean

@@ -337,10 +337,8 @@ maps `Π i, α →o π i`. -/
 def subtype.val (p : α → Prop) : subtype p →o α :=
 ⟨subtype.val, λ x y h, h⟩
 
--- TODO[gh-6025]: make this a global instance once safe to do so
 /-- There is a unique monotone map from a subsingleton to itself. -/
-local attribute [instance]
-def unique [subsingleton α] : unique (α →o α) :=
+instance unique [subsingleton α] : unique (α →o α) :=
 { default := order_hom.id, uniq := λ a, ext _ _ (subsingleton.elim _ _) }
 
 lemma order_hom_eq_id [subsingleton α] (g : α →o α) : g = order_hom.id :=

src/ring_theory/algebraic_independent.lean

@@ -153,8 +153,7 @@ lemma alg_hom.algebraic_independent_iff (f : A →ₐ[R] A') (hf : injective f)
 
 @[nontriviality]
 lemma algebraic_independent_of_subsingleton [subsingleton R] : algebraic_independent R x :=
-by haveI := @mv_polynomial.unique R ι;
-  exact algebraic_independent_iff.2 (λ l hl, subsingleton.elim _ _)
+algebraic_independent_iff.2 (λ l hl, subsingleton.elim _ _)
 
 theorem algebraic_independent_equiv (e : ι ≃ ι') {f : ι' → A} :
   algebraic_independent R (f ∘ e) ↔ algebraic_independent R f :=

src/set_theory/ordinal/fixed_point.lean

@@ -85,7 +85,7 @@ theorem nfp_family_le_fp (H : ∀ i, monotone (f i)) {a b} (ab : a ≤ b) (h : 
   nfp_family f a ≤ b :=
 sup_le $ λ l, begin
   by_cases hι : is_empty ι,
-  { rwa @unique.eq_default _ (@list.unique_of_is_empty ι hι) l },
+  { resetI, rwa unique.eq_default l },
   { haveI := not_is_empty_iff.1 hι,
     induction l with i l IH generalizing a, {exact ab},
     exact (H i (IH ab)).trans (h i) }

src/topology/continuous_function/algebra.lean

@@ -681,8 +681,7 @@ end
 
 end continuous_map
 
--- TODO[gh-6025]: make this an instance once safe to do so
-lemma continuous_map.subsingleton_subalgebra (α : Type*) [topological_space α]
+instance continuous_map.subsingleton_subalgebra (α : Type*) [topological_space α]
   (R : Type*) [comm_semiring R] [topological_space R] [topological_semiring R]
   [subsingleton α] : subsingleton (subalgebra R C(α, R)) :=
 begin

src/topology/continuous_function/weierstrass.lean

@@ -78,7 +78,6 @@ begin
     -- so all subalgebras are the same anyway.
     haveI : subsingleton (set.Icc a b) := ⟨λ x y, le_antisymm
       ((x.2.2.trans (not_lt.mp h)).trans y.2.1) ((y.2.2.trans (not_lt.mp h)).trans x.2.1)⟩,
-    haveI := (continuous_map.subsingleton_subalgebra (set.Icc a b) ℝ),
     apply subsingleton.elim, }
 end
 

src/topology/metric_space/basic.lean

@@ -2719,8 +2719,6 @@ metric_space.induced coe subtype.coe_injective ‹_›
 @[to_additive] instance {α : Type*} [metric_space α] : metric_space (αᵐᵒᵖ) :=
 metric_space.induced mul_opposite.unop mul_opposite.unop_injective ‹_›
 
-local attribute [instance] filter.unique
-
 instance : metric_space empty :=
 { dist := λ _ _, 0,
   dist_self := λ _, rfl,