Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 66c00d33d47b75171f9261e26c602b326202b67a --onto 02f7a1dd41f034939acf49a5c2c590076cb26d8e. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-24 14:38:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68d9d14d44ec95afe26968fff7a682968b2d2fb9 --onto 02f7a1dd41f034939acf49a5c2c590076cb26d8e. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-25 09:44:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8195f7050283953d361e221d74c7607f6396b0d7 --onto 416e07a68e5d9b884de8af4836497a7cc2414c8f. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-25 17:04:25)

!bench

Here are the benchmark results for commit 008d4c7.
The entire run failed.
Found no significant differences.

!bench

Here are the benchmark results for commit 5a123dc.
The entire run failed.
Found no significant differences.

I imagine that changing theorems to axioms will cause quite a few problems -- an alternative I see that might be less intrusive is to replace the body with some dummy value like _proof_omitted. The advantage is obviously that we need to refactor less parts of code to treat the case of theorems without an imported body. The disadvantage is obviously that the resulting term is not type-correct, an alternative is to use lcProof so at least it's type-correct except it's unsafe within a safe declaration. Then it would at least be easy to detect (TheoremInfo.isProofOmitted := value == lcProof very roughly). Not sure what works best, maybe we'd want to add a new unsafe axiom particularly for this case even..?

Also I guess this could get weird w.r.t. #print axioms... If theorems become axioms then suddenly everything is an axiom, if theorems stay theorems but have their body change to a dummy value then suddenly sorry proofs depend on no axioms..? One really bad hack would be to instead replace the bodies with proofOmitted @Classical.choice @Quot.sound @propext depending on which axioms are used but I'm not sure what to think of that...

Thanks for thinking through this!

I imagine that changing theorems to axioms will cause quite a few problems

Do you have some specific concerns in mind? Current evidence suggests the opposite, the transitive uses of thmInfo patterns are surprisingly few.

Also I guess this could get weird w.r.t. #print axioms

Look forward to a follow-up PR introducing an environment extension for this. This was the only non-trivial thmInfo use case I found in core.

Hmm I guess I can't really say much about where thmInfo is used either but the hack in MutualDef is definitely not nice (in particular for matching on syntax). I'm not 100% sold on @[dsimp] (well that is, depending on how it would work). Just a @[dsimp] tag instead of @[simp] would definitely not work well because

1. what about other simp attributes?
2. how about non-simp theorems that are still rfl and used in simp calls? (_def lemmas come to mind)

One way that you could address these would definitely be to make @[dsimp] an additional tag (so @[simp, dsimp]) and the @[dsimp] extension is just a set of those theorems without structure (so that when you add a lemma to simp, it can check whether it is in this set).
That would work but it requires the foresight to tag all defeq lemmas that you might want to use in dsimp with @[dsimp] so not great either.

@nomeata will work on the [dsimp] part separately

!bench

Here are the benchmark results for commit 205d08d.
There were significant changes against commit 68d9d14:

  Benchmark                      Metric                       Change
  =============================================================================
+ Init size                      bytes .olean                 -55.1%
- Init size                      bytes .olean.private      283914.3%
- Init.Data.BitVec.Lemmas        branch-misses                 64.3%  (268.9 σ)
- Init.Data.BitVec.Lemmas        branches                      12.8%  (227.4 σ)
- Init.Data.BitVec.Lemmas        instructions                  14.4%  (227.3 σ)
- Init.Data.BitVec.Lemmas        maxrss                        53.6%   (23.0 σ)
- Init.Data.BitVec.Lemmas        task-clock                    87.9% (1561.4 σ)
+ Init.Data.BitVec.Lemmas        wall-clock                   -25.7% (-506.0 σ)
+ Init.Data.List.Sublist async   branches                      -4.5%  (-38.4 σ)
+ Init.Data.List.Sublist async   instructions                  -5.0%  (-37.4 σ)
+ Init.Data.List.Sublist async   task-clock                   -20.5%  (-26.2 σ)
- Init.Data.List.Sublist async   wall-clock                    15.0%   (12.9 σ)
+ bv_decide_large_aig.lean       task-clock                    -5.6%  (-19.5 σ)
+ bv_decide_large_aig.lean       wall-clock                    -5.5%  (-23.3 σ)
- identifier auto-completion     branches                       3.1%  (905.5 σ)
- identifier auto-completion     instructions                   2.7% (1147.7 σ)
+ import Lean                    task-clock                    -3.8%  (-24.0 σ)
+ import Lean                    wall-clock                    -3.7%  (-31.6 σ)
+ parser                         task-clock                    -2.3%  (-10.4 σ)
+ parser                         wall-clock                    -2.3%  (-10.3 σ)
- qsort                          task-clock                     2.3%   (15.9 σ)
- qsort                          wall-clock                     2.3%   (15.8 σ)
- reduceMatch                    task-clock                     1.9%   (11.5 σ)
+ stdlib                         blocked                      -21.8%  (-69.2 σ)
- stdlib                         dsimp                          5.6%  (279.7 σ)
- stdlib                         maxrss                         9.9%   (11.1 σ)
- stdlib                         process pre-definitions        7.0%   (18.7 σ)
- stdlib                         tactic execution              13.0%  (209.5 σ)
- stdlib                         task-clock                     5.1%  (108.9 σ)
- stdlib                         type checking                  4.1%   (65.5 σ)
+ stdlib size                    bytes .olean                  -9.8%
- stdlib size                    bytes .olean.private      283914.3%