From b95b8c7a484a298228805c72c142f6b062eb0d70 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 16 Aug 2022 10:36:58 +0000 Subject: [PATCH] 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](https://github.com/leanprover-community/lean/pull/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](https://github.com/leanprover-community/mathlib/commit/c7626b7dfe2bf35b48cf43178a32d74f5dbf8b3f#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 | 3 +- src/algebra/algebra/subalgebra/basic.lean | 31 ++++--------------- src/algebra/lie/solvable.lean | 2 +- src/algebra/lie/subalgebra.lean | 3 +- src/algebra/lie/submodule.lean | 6 ++-- src/algebra/module/basic.lean | 6 ++-- src/algebra/order/complete_field.lean | 2 -- src/algebra/order/hom/ring.lean | 13 ++------ src/analysis/normed_space/multilinear.lean | 4 --- src/data/list/basic.lean | 3 +- src/data/matrix/basic.lean | 6 ++-- src/data/matrix/dmatrix.lean | 6 ++-- src/data/mv_polynomial/basic.lean | 3 +- src/geometry/manifold/charted_space.lean | 6 ---- src/linear_algebra/matrix/adjugate.lean | 4 +-- .../matrix/charpoly/finite_field.lean | 4 +-- src/logic/basic.lean | 4 +-- src/number_theory/cyclotomic/basic.lean | 4 +-- src/number_theory/cyclotomic/rat.lean | 1 - src/number_theory/number_field.lean | 3 -- src/order/filter/basic.lean | 4 +-- src/order/hom/basic.lean | 4 +-- src/ring_theory/algebraic_independent.lean | 3 +- src/set_theory/ordinal/fixed_point.lean | 2 +- src/topology/continuous_function/algebra.lean | 3 +- .../continuous_function/weierstrass.lean | 1 - src/topology/metric_space/basic.lean | 2 -- 27 files changed, 34 insertions(+), 99 deletions(-) diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean index d699d267f66d9..b04697f5de8a4 100644 --- a/src/algebra/algebra/basic.lean +++ b/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 _ _⟩ diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean index 7d8d4bb89d90a..890bf221c604b 100644 --- a/src/algebra/algebra/subalgebra/basic.lean +++ b/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 diff --git a/src/algebra/lie/solvable.lean b/src/algebra/lie/solvable.lean index 88bb281acdadd..4dfacb432f908 100644 --- a/src/algebra/lie/solvable.lean +++ b/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) := diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean index cf504b3d258d5..dc2c5a405795d 100644 --- a/src/algebra/lie/subalgebra.lean +++ b/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, diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean index 340822d8408d9..41df037476c8d 100644 --- a/src/algebra/lie/submodule.lean +++ b/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, diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean index 64ef7765defbf..c755d1e885709 100644 --- a/src/algebra/module/basic.lean +++ b/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⟩ diff --git a/src/algebra/order/complete_field.lean b/src/algebra/order/complete_field.lean index cfbffd072e590..3445eee9388a3 100644 --- a/src/algebra/order/complete_field.lean +++ b/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 α β diff --git a/src/algebra/order/hom/ring.lean b/src/algebra/order/hom/ring.lean index 7fbd7a488e2c5..f5cdb1c1f7c13 100644 --- a/src/algebra/order/hom/ring.lean +++ b/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 diff --git a/src/analysis/normed_space/multilinear.lean b/src/analysis/normed_space/multilinear.lean index 6536964a175d8..e05e646fb5f64 100644 --- a/src/analysis/normed_space/multilinear.lean +++ b/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'} diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index 68a9c3226b0db..1d2e00858677a 100644 --- a/src/data/list/basic.lean +++ b/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 diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 9da0bdad20444..691637101217d 100644 --- a/src/data/matrix/basic.lean +++ b/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 diff --git a/src/data/matrix/dmatrix.lean b/src/data/matrix/dmatrix.lean index dba9388a84365..a8a0854578708 100644 --- a/src/data/matrix/dmatrix.lean +++ b/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 diff --git a/src/data/mv_polynomial/basic.lean b/src/data/mv_polynomial/basic.lean index 2c2b9d802150a..fc988106a70be 100644 --- a/src/data/mv_polynomial/basic.lean +++ b/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 diff --git a/src/geometry/manifold/charted_space.lean b/src/geometry/manifold/charted_space.lean index 1787d7f5117b1..d7733b339616e 100644 --- a/src/geometry/manifold/charted_space.lean +++ b/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-/ diff --git a/src/linear_algebra/matrix/adjugate.lean b/src/linear_algebra/matrix/adjugate.lean index 3e7cd5e98a9f2..1667cb28db521 100644 --- a/src/linear_algebra/matrix/adjugate.lean +++ b/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, diff --git a/src/linear_algebra/matrix/charpoly/finite_field.lean b/src/linear_algebra/matrix/charpoly/finite_field.lean index e701a3d07ed0d..010277b4b321c 100644 --- a/src/linear_algebra/matrix/charpoly/finite_field.lean +++ b/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)) : diff --git a/src/logic/basic.lean b/src/logic/basic.lean index 2d01cf741fd7a..0a712ccba10a8 100644 --- a/src/logic/basic.lean +++ b/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 diff --git a/src/number_theory/cyclotomic/basic.lean b/src/number_theory/cyclotomic/basic.lean index 272d708e4da32..f323dcc6e0948 100644 --- a/src/number_theory/cyclotomic/basic.lean +++ b/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` diff --git a/src/number_theory/cyclotomic/rat.lean b/src/number_theory/cyclotomic/rat.lean index e71acd34ee2c9..0b065fea48e53 100644 --- a/src/number_theory/cyclotomic/rat.lean +++ 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) ℤ ℚ`. -/ diff --git a/src/number_theory/number_field.lean b/src/number_theory/number_field.lean index ca2642b27dc14..0a498877123d4 100644 --- a/src/number_theory/number_field.lean +++ b/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. -/ diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index 0cb5388330dc7..85569c1cc42f0 100644 --- a/src/order/filter/basic.lean +++ b/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 diff --git a/src/order/hom/basic.lean b/src/order/hom/basic.lean index adab1a0159ebf..5607f8afbb337 100644 --- a/src/order/hom/basic.lean +++ b/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 := diff --git a/src/ring_theory/algebraic_independent.lean b/src/ring_theory/algebraic_independent.lean index 0ee9b87995b14..2cafbefcdae84 100644 --- a/src/ring_theory/algebraic_independent.lean +++ b/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 := diff --git a/src/set_theory/ordinal/fixed_point.lean b/src/set_theory/ordinal/fixed_point.lean index f835a513fc28e..5d54671f85016 100644 --- a/src/set_theory/ordinal/fixed_point.lean +++ b/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) } diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean index 3df7a64e0964a..1fdde95a636b9 100644 --- a/src/topology/continuous_function/algebra.lean +++ b/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 diff --git a/src/topology/continuous_function/weierstrass.lean b/src/topology/continuous_function/weierstrass.lean index 665260cde375d..6cf001aa8dfed 100644 --- a/src/topology/continuous_function/weierstrass.lean +++ b/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 diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index a08b776e6efbe..83c247b574e2c 100644 --- a/src/topology/metric_space/basic.lean +++ b/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,