cleanup(*): use priority 10 for low priority

src/analysis/calculus/deriv.lean

@@ -53,7 +53,7 @@ import analysis.asymptotics analysis.calculus.tangent_cone
 open filter asymptotics continuous_linear_map set
 
 noncomputable theory
-local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable
+local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable
 
 set_option class.instance_max_depth 90
 

src/analysis/calculus/times_cont_diff.lean

@@ -66,7 +66,7 @@ derivative, differentiability, higher derivative, C^n
 -/
 
 noncomputable theory
-local attribute [instance, priority 0] classical.decidable_inhabited classical.prop_decidable
+local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable
 
 universes u v w
 

src/category/bifunctor.lean

@@ -108,11 +108,11 @@ by refine { .. }; intros; cases x; refl
 
 open bifunctor functor
 
-@[priority 0]
+@[priority 10]
 instance bifunctor.functor {α} : functor (F α) :=
 { map := λ _ _, snd }
 
-@[priority 0]
+@[priority 10]
 instance bifunctor.is_lawful_functor [is_lawful_bifunctor F] {α} : is_lawful_functor (F α) :=
 by refine {..}; intros; simp [functor.map] with functor_norm
 

src/category/bitraversable/instances.lean

@@ -83,11 +83,11 @@ by constructor; introsI; casesm is_lawful_bitraversable t; apply_assumption
 
 open bitraversable functor
 
-@[priority 0]
+@[priority 10]
 instance bitraversable.traversable {α} : traversable (t α) :=
 { traverse := @tsnd t _ _ }
 
-@[priority 0]
+@[priority 10]
 instance bitraversable.is_lawful_traversable [is_lawful_bitraversable t] {α} :
   is_lawful_traversable (t α) :=
 by { constructor; introsI; simp [traverse,comp_tsnd] with functor_norm,

src/category_theory/adjunction/basic.lean

@@ -46,21 +46,21 @@ namespace adjunction
 
 restate_axiom hom_equiv_unit'
 restate_axiom hom_equiv_counit'
-attribute [simp, priority 1] hom_equiv_unit hom_equiv_counit
+attribute [simp, priority 10] hom_equiv_unit hom_equiv_counit
 
 section
 
 variables {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) {X' X : C} {Y Y' : D}
 
-@[simp, priority 1] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
+@[simp, priority 10] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
   (adj.hom_equiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.hom_equiv X Y).symm g :=
 by rw [hom_equiv_counit, F.map_comp, assoc, adj.hom_equiv_counit.symm]
 
 @[simp] lemma hom_equiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
   (adj.hom_equiv X' Y) (F.map f ≫ g) = f ≫ (adj.hom_equiv X Y) g :=
 by rw [← equiv.eq_symm_apply]; simp [-hom_equiv_unit]
 
-@[simp, priority 1] lemma hom_equiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
+@[simp, priority 10] lemma hom_equiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
   (adj.hom_equiv X Y') (f ≫ g) = (adj.hom_equiv X Y) f ≫ G.map g :=
 by rw [hom_equiv_unit, G.map_comp, ← assoc, ←hom_equiv_unit]
 
@@ -117,7 +117,7 @@ namespace core_hom_equiv
 
 restate_axiom hom_equiv_naturality_left_symm'
 restate_axiom hom_equiv_naturality_right'
-attribute [simp, priority 1] hom_equiv_naturality_left_symm hom_equiv_naturality_right
+attribute [simp, priority 10] hom_equiv_naturality_left_symm hom_equiv_naturality_right
 
 variables {F : C ⥤ D} {G : D ⥤ C} (adj : core_hom_equiv F G) {X' X : C} {Y Y' : D}
 

src/computability/primrec.lean

@@ -108,7 +108,7 @@ class primcodable (α : Type*) extends encodable α :=
 namespace primcodable
 open nat.primrec
 
-@[priority 0] instance of_denumerable (α) [denumerable α] : primcodable α :=
+@[priority 10] instance of_denumerable (α) [denumerable α] : primcodable α :=
 ⟨succ.of_eq $ by simp⟩
 
 def of_equiv (α) {β} [primcodable α] (e : β ≃ α) : primcodable β :=

src/data/fintype.lean

@@ -196,7 +196,7 @@ instance (n : ℕ) : fintype (fin n) :=
 @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
 by rw [fin.fintype]; simp [fintype.card, card, univ]
 
-@[instance, priority 0] def unique.fintype {α : Type*} [unique α] : fintype α :=
+@[instance, priority 10] def unique.fintype {α : Type*} [unique α] : fintype α :=
 ⟨finset.singleton (default α), λ x, by rw [unique.eq_default x]; simp⟩
 
 @[simp] lemma univ_unique {α : Type*} [unique α] [f : fintype α] : @finset.univ α _ = {default α} :=
@@ -712,7 +712,7 @@ subrelation.wf this (measure_wf _)
 lemma preorder.well_founded [fintype α] [preorder α] : well_founded ((<) : α → α → Prop) :=
 well_founded_of_trans_of_irrefl _
 
-@[instance, priority 0] lemma linear_order.is_well_order [fintype α] [linear_order α] :
+@[instance, priority 10] lemma linear_order.is_well_order [fintype α] [linear_order α] :
   is_well_order α (<) :=
 { wf := preorder.well_founded }
 

src/data/int/basic.lean

@@ -1048,7 +1048,7 @@ protected def cast : ℤ → α
 | (n : ℕ) := n
 | -[1+ n] := -(n+1)
 
-@[priority 0] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩
+@[priority 10] instance cast_coe : has_coe ℤ α := ⟨int.cast⟩
 
 @[simp, squash_cast] theorem cast_zero : ((0 : ℤ) : α) = 0 := rfl
 

src/data/nat/cast.lean

@@ -19,7 +19,7 @@ protected def cast : ℕ → α
 | 0     := 0
 | (n+1) := cast n + 1
 
-@[priority 0] instance cast_coe : has_coe ℕ α := ⟨nat.cast⟩
+@[priority 10] instance cast_coe : has_coe ℕ α := ⟨nat.cast⟩
 
 @[simp, squash_cast] theorem cast_zero : ((0 : ℕ) : α) = 0 := rfl
 

src/data/num/basic.lean

@@ -160,9 +160,9 @@ section
   | 0           := 0
   | (num.pos p) := cast_pos_num p
 
-  @[priority 0] instance pos_num_coe : has_coe pos_num α := ⟨cast_pos_num⟩
+  @[priority 10] instance pos_num_coe : has_coe pos_num α := ⟨cast_pos_num⟩
 
-  @[priority 0] instance num_nat_coe : has_coe num α := ⟨cast_num⟩
+  @[priority 10] instance num_nat_coe : has_coe num α := ⟨cast_num⟩
 
   instance : has_repr pos_num := ⟨λ n, repr (n : ℕ)⟩
   instance : has_repr num := ⟨λ n, repr (n : ℕ)⟩
@@ -504,7 +504,7 @@ section
   | (znum.pos p) := p
   | (znum.neg p) := -p
 
-  @[priority 0] instance znum_coe : has_coe znum α := ⟨cast_znum⟩
+  @[priority 10] instance znum_coe : has_coe znum α := ⟨cast_znum⟩
 
   instance : has_repr znum := ⟨λ n, repr (n : ℤ)⟩
 end

src/data/rat/cast.lean

@@ -35,7 +35,7 @@ variable [division_ring α]
 protected def cast : ℚ → α
 | ⟨n, d, h, c⟩ := n / d
 
-@[priority 0] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩
+@[priority 10] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩
 
 @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n :=
 show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]

src/field_theory/splitting_field.lean

@@ -118,7 +118,7 @@ is_noetherian_ring.irreducible_induction_on (f.map i)
 
 section UFD
 
-local attribute [instance, priority 0] principal_ideal_domain.to_unique_factorization_domain
+local attribute [instance, priority 10] principal_ideal_domain.to_unique_factorization_domain
 local infix ` ~ᵤ ` : 50 := associated
 
 open unique_factorization_domain associates

src/group_theory/sylow.lean

@@ -11,7 +11,7 @@ open equiv.perm is_subgroup list quotient_group
 universes u v w
 variables {G : Type u} {α : Type v} {β : Type w} [group G]
 
-local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable
+local attribute [instance, priority 10] subtype.fintype set_fintype classical.prop_decidable
 
 namespace mul_action
 variables [mul_action G α]

src/linear_algebra/finsupp.lean

@@ -8,7 +8,7 @@ Linear structures on function with finite support `α →₀ β`.
 import data.finsupp linear_algebra.basic
 
 noncomputable theory
-local attribute [instance, priority 0] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 
 open lattice set linear_map submodule
 

src/logic/basic.lean

@@ -31,7 +31,7 @@ instance : subsingleton empty := ⟨λa, a.elim⟩
 
 instance : decidable_eq empty := λa, a.elim
 
-@[priority 0] instance decidable_eq_of_subsingleton
+@[priority 10] instance decidable_eq_of_subsingleton
   {α} [subsingleton α] : decidable_eq α
 | a b := is_true (subsingleton.elim a b)
 

src/logic/function.lean

@@ -94,7 +94,7 @@ theorem right_inverse.comp {γ} {f : α → β} {g : β → α} {h : β → γ}
   (hf : right_inverse f g) (hh : right_inverse h i) : right_inverse (h ∘ f) (g ∘ i) :=
 left_inverse.comp hh hf
 
-local attribute [instance, priority 1] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 
 /-- We can use choice to construct explicitly a partial inverse for
   a given injective function `f`. -/
@@ -119,7 +119,7 @@ end
 section inv_fun
 variables {α : Type u} [inhabited α] {β : Sort v} {f : α → β} {s : set α} {a : α} {b : β}
 
-local attribute [instance, priority 1] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 
 /-- Construct the inverse for a function `f` on domain `s`. -/
 noncomputable def inv_fun_on (f : α → β) (s : set α) (b : β) : α :=

src/tactic/finish.lean

@@ -111,7 +111,7 @@ variable  {α : Type u}
 variables (p q : Prop)
 variable  (s : α → Prop)
 
-local attribute [instance, priority 1] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 theorem not_not_eq : (¬ ¬ p) = p := propext not_not
 theorem not_and_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_distrib
 theorem not_or_eq : (¬ (p ∨ q)) = (¬ p ∧ ¬ q) := propext not_or_distrib
@@ -397,7 +397,7 @@ local_context >>= case_some_hyp_aux s cont
   `safe_core s ps cfg opt` negates the goal, normalizes hypotheses
   (by splitting conjunctions, eliminating existentials, pushing negations inwards,
   and calling `simp` with the supplied lemmas `s`), and then tries `contradiction`.
-  
+
   If this fails, it will create an SMT state and repeatedly use `ematch`
   (using `ematch` lemmas in the environment, universally quantified assumptions,
   and the supplied lemmas `ps`) and congruence closure.
@@ -432,7 +432,7 @@ do when_tracing `auto.finish (trace "entering safe_core" >> trace_state),
 
 /--
   `clarify` is `safe_core`, but with the `(opt : case_option)`
-  parameter fixed at `case_option.at_most_one`. 
+  parameter fixed at `case_option.at_most_one`.
 -/
 meta def clarify (s : simp_lemmas × list name) (ps : list pexpr)
   (cfg : auto_config := {}) : tactic unit := safe_core s ps cfg case_option.at_most_one
@@ -481,13 +481,13 @@ local postfix *:9001 := many
   `clarify [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses
   (by splitting conjunctions, eliminating existentials, pushing negations inwards,
   and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`.
-  
+
   If this fails, it will create an SMT state and repeatedly use `ematch`
   (using `ematch` lemmas in the environment, universally quantified assumptions,
   and the supplied lemmas `e1,...,en`) and congruence closure.
 
   `clarify` is complete for propositional logic.
-  
+
   Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
 
   `clarify` will fail if it produces more than one goal.
@@ -501,13 +501,13 @@ do s ← mk_simp_set ff [] hs,
   `safe [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses
   (by splitting conjunctions, eliminating existentials, pushing negations inwards,
   and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`.
-  
+
   If this fails, it will create an SMT state and repeatedly use `ematch`
   (using `ematch` lemmas in the environment, universally quantified assumptions,
   and the supplied lemmas `e1,...,en`) and congruence closure.
 
   `safe` is complete for propositional logic.
-  
+
   Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
 
   `safe` ignores the number of goals it produces, and should never fail.
@@ -521,13 +521,13 @@ do s ← mk_simp_set ff [] hs,
   `finish [h1,...,hn] using [e1,...,en]` negates the goal, normalizes hypotheses
   (by splitting conjunctions, eliminating existentials, pushing negations inwards,
   and calling `simp` with the supplied lemmas `h1,...,hn`), and then tries `contradiction`.
-  
+
   If this fails, it will create an SMT state and repeatedly use `ematch`
   (using `ematch` lemmas in the environment, universally quantified assumptions,
   and the supplied lemmas `e1,...,en`) and congruence closure.
 
   `finish` is complete for propositional logic.
-  
+
   Either of the supplied simp lemmas or the supplied ematch lemmas are optional.
 
   `finish` will fail if it does not close the goal.

src/tactic/localized.lean

@@ -70,7 +70,7 @@ meta def print_localized_commands (ns : list name) : tactic unit :=
 do cmds ← get_localized ns, cmds.mmap' trace
 
 -- you can run `open_locale classical` to get the decidability of all propositions.
-localized "attribute [instance, priority 1] classical.prop_decidable" in classical
+localized "attribute [instance, priority 9] classical.prop_decidable" in classical
 
 localized "postfix `?`:9001 := optional" in parser
 localized "postfix *:9001 := lean.parser.many" in parser

src/tactic/push_neg.lean

@@ -21,7 +21,7 @@ variable  {α : Sort u}
 variables (p q : Prop)
 variable  (s : α → Prop)
 
-local attribute [instance, priority 1] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 theorem not_not_eq : (¬ ¬ p) = p := propext not_not
 theorem not_and_eq : (¬ (p ∧ q)) = (¬ p ∨ ¬ q) := propext not_and_distrib
 theorem not_or_eq : (¬ (p ∨ q)) = (¬ p ∧ ¬ q) := propext not_or_distrib

src/topology/algebra/uniform_group.lean

@@ -61,7 +61,7 @@ by simp * at *
 lemma uniform_continuous_add' : uniform_continuous (λp:α×α, p.1 + p.2) :=
 uniform_continuous_add uniform_continuous_fst uniform_continuous_snd
 
-@[priority 0]
+@[priority 10]
 instance uniform_add_group.to_topological_add_group : topological_add_group α :=
 { continuous_add := uniform_continuous_add'.continuous,
   continuous_neg := uniform_continuous_neg'.continuous }

src/topology/metric_space/gromov_hausdorff.lean

@@ -225,7 +225,7 @@ begin
   simp [Aα, Bβ]
 end
 
-local attribute [instance, priority 0] inhabited_of_nonempty'
+local attribute [instance, priority 10] inhabited_of_nonempty'
 
 /-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
 essentially by design. -/
@@ -371,8 +371,8 @@ end
 
 -- without the next two lines, { exact closed_of_compact (range Φ) hΦ } in the next
 -- proof is very slow, as the t2_space instance is very hard to find
-local attribute [instance, priority 0] orderable_topology.t2_space
-local attribute [instance, priority 0] ordered_topology.to_t2_space
+local attribute [instance, priority 10] orderable_topology.t2_space
+local attribute [instance, priority 10] ordered_topology.to_t2_space
 
 /-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
 instance GH_space_metric_space : metric_space GH_space :=

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -66,7 +66,7 @@ section constructions
 variables {α : Type u} {β : Type v}
 [metric_space α] [compact_space α] [nonempty α] [metric_space β] [compact_space β] [nonempty β]
 {f : prod_space_fun α β} {x y z t : α ⊕ β}
-local attribute [instance, priority 0] inhabited_of_nonempty'
+local attribute [instance, priority 10] inhabited_of_nonempty'
 
 private lemma max_var_bound : dist x y ≤ max_var α β := calc
   dist x y ≤ diam (univ : set (α ⊕ β)) :

src/topology/uniform_space/abstract_completion.lean

@@ -45,7 +45,7 @@ uniform spaces, completion, universal property
 -/
 
 noncomputable theory
-local attribute [instance, priority 0] classical.prop_decidable
+local attribute [instance, priority 10] classical.prop_decidable
 
 open filter set function