fix(logic/basic): remove noncomputable lemma (#10292)

It's been three years since this was discussed according to the zulip archive link in the library note.

According to CI, the reason is no longer relevant. Leaving these as `noncomputable lemma` is harmful as it results in non-defeq instance diamonds sometimes as lean was not able to unfold the lemmas to get to the data underneath.

Since these are now `def`s, the linter requires them to have docstrings.

src/logic/basic.lean

@@ -1145,26 +1145,19 @@ theorem cases {p : Prop → Prop} (h1 : p true) (h2 : p false) : ∀a, p a :=
 assume a, cases_on a h1 h2
 
 /- use shortened names to avoid conflict when classical namespace is open. -/
-noncomputable lemma dec (p : Prop) : decidable p := -- see Note [classical lemma]
+/-- Any prop `p` is decidable classically. A shorthand for `classical.prop_decidable`. -/
+noncomputable def dec (p : Prop) : decidable p :=
 by apply_instance
-noncomputable lemma dec_pred (p : α → Prop) : decidable_pred p := -- see Note [classical lemma]
+/-- Any predicate `p` is decidable classically. -/
+noncomputable def dec_pred (p : α → Prop) : decidable_pred p :=
 by apply_instance
-noncomputable lemma dec_rel (p : α → α → Prop) : decidable_rel p := -- see Note [classical lemma]
+/-- Any relation `p` is decidable classically. -/
+noncomputable def dec_rel (p : α → α → Prop) : decidable_rel p :=
 by apply_instance
-noncomputable lemma dec_eq (α : Sort*) : decidable_eq α := -- see Note [classical lemma]
+/-- Any type `α` has decidable equality classically. -/
+noncomputable def dec_eq (α : Sort*) : decidable_eq α :=
 by apply_instance
 
-/--
-We make decidability results that depends on `classical.choice` noncomputable lemmas.
-* We have to mark them as noncomputable, because otherwise Lean will try to generate bytecode
-  for them, and fail because it depends on `classical.choice`.
-* We make them lemmas, and not definitions, because otherwise later definitions will raise
-  \"failed to generate bytecode\" errors when writing something like
-  `letI := classical.dec_eq _`.
-Cf. <https://leanprover-community.github.io/archive/stream/113488-general/topic/noncomputable.20theorem.html>
--/
-library_note "classical lemma"
-
 /-- Construct a function from a default value `H0`, and a function to use if there exists a value
 satisfying the predicate. -/
 @[elab_as_eliminator]

src/tactic/lint/misc.lean

@@ -251,8 +251,6 @@ has been used. -/
   no_errors_found := "All declarations correctly marked as def/lemma.",
   errors_found := "INCORRECT DEF/LEMMA:" }
 
-attribute [nolint def_lemma] classical.dec classical.dec_pred classical.dec_rel classical.dec_eq
-
 /-!
 ## Linter that checks whether declarations are well-typed
 -/