fix: remove compile_inductive% False (leanprover-community#32225)

Per `hargoniX` [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Error.20when.20executing.20files.20with.20Mathlib.20import/near/560729156):

This issue occurs due to two factors. The first is the module system that changed the behavior of the inliner for, so far, unknown reasons. However, the behavior of compile_inductive% on False has always been wrong to begin with and so far merely been fixed by the inliner by chance. First things first, it is unnecessary to even compile_inductive% False because False.rec is the single recursor that the compiler has native support for. The reason that calling compile_inductive% on it causes an issue, is that it introduces a new constant False.rec' = unreach. This constant used to be inlined but with the new module system does not get inlined for some reason. Because of this, the compiler decides to closed term lift it and we end up executing an unreachable during initialization. This behavior is a known limitation/bug of the current closed term extraction feature.

The correct fix would be for mathlib to either stop calling compile_inductive% on False as it is actively harming compiler optimizations and unnecessary or to at least place a @[no_extract] attribute on the False.rec' that compile_inductive% generates. This attribute informs the closed term extractor that it is not supposed to pull the constant out and is also placed on other always crashing symbols like panic! or unreachable!.

Author: Ruben-VandeVelde

Mathlib/Util/CompileInductive.lean

@@ -247,7 +247,6 @@ compile_inductive% PEmpty
 compile_inductive% Sum
 compile_inductive% PSum
 compile_inductive% And
-compile_inductive% False
 compile_inductive% Empty
 compile_inductive% Bool
 compile_inductive% Sigma

MathlibTest/CompileInductive.lean

@@ -15,7 +15,6 @@ example := @Fin2.recOn
 example := @PUnit.recOn
 example := @PEmpty.recOn
 example := @And.recOn
-example := @False.recOn
 example := @Empty.recOn
 
 example := @Nat.brecOn