chore(data/nat/prime): fact (2.prime) (#10441)

Co-authored-by: Eric <ericrboidi@gmail.com>

src/data/nat/prime.lean

@@ -1030,6 +1030,12 @@ namespace nat
 
 theorem prime_three : prime 3 := by norm_num
 
+/-- See note [fact non-instances].-/
+lemma fact_prime_two : fact (prime 2) := ⟨prime_two⟩
+
+/-- See note [fact non-instances].-/
+lemma fact_prime_three : fact (prime 3) := ⟨prime_three⟩
+
 end nat
 
 

src/logic/basic.lean

@@ -190,6 +190,13 @@ In particular, this class is not intended for turning the type class system
 into an automated theorem prover for first order logic. -/
 class fact (p : Prop) : Prop := (out [] : p)
 
+/--
+In most cases, we should not have global instances of `fact`; typeclass search only reads the head
+symbol and then tries any instances, which means that adding any such instance will cause slowdowns
+everywhere. We instead make them as lemmata and make them local instances as required.
+-/
+library_note "fact non-instances"
+
 lemma fact.elim {p : Prop} (h : fact p) : p := h.1
 lemma fact_iff {p : Prop} : fact p ↔ p := ⟨λ h, h.1, λ h, ⟨h⟩⟩
 

src/number_theory/quadratic_reciprocity.lean

@@ -429,9 +429,7 @@ have hqp0 : (q : zmod p) ≠ 0, from prime_ne_zero p q hpq,
 by rw [eisenstein_lemma q hp1.1 hpq0, eisenstein_lemma p hq1.1 hqp0,
   ← pow_add, sum_mul_div_add_sum_mul_div_eq_mul q p hpq0, mul_comm]
 
--- move this
-local attribute [instance]
-lemma fact_prime_two : fact (nat.prime 2) := ⟨nat.prime_two⟩
+local attribute [instance] nat.fact_prime_two
 
 lemma legendre_sym_two [hp1 : fact (p % 2 = 1)] : legendre_sym 2 p = (-1) ^ (p / 4 + p / 2) :=
 have hp2 : p ≠ 2, from mt (congr_arg (% 2)) (by simpa using hp1.1),