chore(*): fix errors in library and sanity_check

src/logic/basic.lean

@@ -591,12 +591,23 @@ begin
   simp only [imp_iff_not_or, or.comm]
 end
 
-/- use shortened names to avoid conflict when classical namespace is open.
-  These are marked as lemmas, to avoid "failed to generate bytecode" errors -/
-noncomputable lemma dec (p : Prop) : decidable p := by apply_instance
-noncomputable lemma dec_pred (p : α → Prop) : decidable_pred p := by apply_instance
-noncomputable lemma dec_rel (p : α → α → Prop) : decidable_rel p := by apply_instance
-noncomputable lemma dec_eq (α : Sort*) : decidable_eq α := by apply_instance
+/- use shortened names to avoid conflict when classical namespace is open. -/
+noncomputable lemma dec (p : Prop) : decidable p := -- see Note [classical lemma]
+by apply_instance
+noncomputable lemma dec_pred (p : α → Prop) : decidable_pred p := -- see Note [classical lemma]
+by apply_instance
+noncomputable lemma dec_rel (p : α → α → Prop) : decidable_rel p := -- see Note [classical lemma]
+by apply_instance
+noncomputable lemma dec_eq (α : Sort*) : decidable_eq α := -- see Note [classical lemma]
+by apply_instance
+
+/- Note [classical lemma]:
+  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 declarations will raise
+    "failed to generate bytecode" errors.
+  Cf. https://leanprover-community.github.io/archive/113488general/08268noncomputabletheorem.html -/
 
 @[elab_as_eliminator]
 noncomputable def {u} exists_cases {C : Sort u} (H0 : C) (H : ∀ a, p a → C) : C :=