feat: abstractNestedProofs in declaration types

[nomeata]

This PR abstracts nested proofs in declaration types. This reduces the size of the goal, and subsequent tactics that massage the goal (in particular match) will have less work to do and produde smaller proof term. The size of the olean of Vector.Extract goes down from 20MB to 5MB with this.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-7345 build failed against this PR. (2025-03-05 12:14:14) View Log
• 💥 Mathlib branch lean-pr-testing-7345 build failed against this PR. (2025-03-05 15:33:37) View Log

[Kha]

!bench

[leanprover-bot]

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

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 911080a.
There were significant changes against commit e3c6909:

  Benchmark                   Metric                    Change
  ========================================================================
+ big_do                      maxrss                     -1.1%   (-49.8 σ)
+ big_omega.lean              branches                   -2.2%   (-77.7 σ)
+ big_omega.lean              instructions               -2.2%  (-109.4 σ)
+ big_omega.lean              maxrss                     -2.0%  (-149.9 σ)
+ big_omega.lean MT           branches                   -2.8%  (-100.8 σ)
+ big_omega.lean MT           instructions               -2.8%  (-120.2 σ)
+ big_omega.lean MT           maxrss                    -13.4%  (-325.4 σ)
- bv_decide_inequality.lean   task-clock                  3.8%    (28.4 σ)
- bv_decide_inequality.lean   wall-clock                  3.8%    (28.6 σ)
+ bv_decide_realworld         maxrss                     -1.2%   (-24.9 σ)
- bv_decide_realworld         task-clock                  3.6%    (16.1 σ)
- bv_decide_realworld         wall-clock                  1.9%    (10.1 σ)
- ilean roundtrip             parse                      10.1%    (28.6 σ)
+ lake config elab            maxrss                     -1.1%   (-17.7 σ)
+ lake config import          maxrss                     -1.1%   (-43.6 σ)
+ lake env                    maxrss                     -1.1%   (-23.4 σ)
+ language server startup     maxrss                     -1.6%   (-13.1 σ)
- liasolver                   task-clock                 10.9%    (13.5 σ)
- liasolver                   wall-clock                 10.9%    (15.3 σ)
- parser                      task-clock                  6.4%    (12.0 σ)
- parser                      wall-clock                  6.4%    (12.0 σ)
- qsort                       task-clock                 10.6%    (22.5 σ)
- qsort                       wall-clock                 10.6%    (22.0 σ)
- rbmap_1                     task-clock                  5.2%    (18.3 σ)
- rbmap_1                     wall-clock                  5.2%    (18.7 σ)
- rbmap_10                    task-clock                  2.3%    (15.6 σ)
- rbmap_10                    wall-clock                  2.3%    (14.4 σ)
- rbmap_fbip                  task-clock                 11.7%    (12.5 σ)
- rbmap_fbip                  wall-clock                 11.8%    (12.9 σ)
+ stdlib                      dsimp                      -8.0%   (-71.3 σ)
+ stdlib                      fix level params          -15.2%  (-168.7 σ)
+ stdlib                      instructions               -4.8% (-1433.6 σ)
+ stdlib                      process pre-definitions   -16.7%   (-36.3 σ)
+ stdlib                      share common exprs        -16.8%   (-22.7 σ)
+ stdlib                      tactic execution          -20.4%  (-186.0 σ)
+ stdlib                      task-clock                 -4.0%   (-29.7 σ)
+ stdlib                      type checking             -12.7%  (-147.6 σ)
+ stdlib size                 bytes .olean               -4.6%
+ workspaceSymbols            task-clock                 -6.5%   (-18.2 σ)
+ workspaceSymbols            wall-clock                 -6.5%   (-18.2 σ)

[nomeata]

#5998 reaped the benefits in a much less invasive way.

Dumping some breakage analysis here for future reference

---

But stage2 doesn’t build.

Somehow simp picks picks a lemma when a proof in its LHS has been abstracted that it wouldn’t pick otherwise, and then we run into a non-confluence.

…

This can be reproduced with rw as well, doesn’t need simp (no branch needed):

theorem map_attach_eq_attachWith_no_abstract {o : Option α} {p : α → Prop} (f : ∀ a, a ∈ o → p a) :
    o.attach.map (fun x => ⟨x.1, f x.1 x.2⟩) = o.attachWith p f := by
  cases o <;> simp_all [Function.comp_def]

theorem map_attach_eq_attachWith_with_abstract {o : Option α} {p : α → Prop} (f : ∀ a, a ∈ o → p a) :
    o.attach.map (fun x => ⟨x.1, by as_aux_lemma => exact f x.1 x.2⟩) = o.attachWith p f := by
  cases o <;> simp_all [Function.comp_def]

example  {o : Option α} {p q : α → Prop} (f : ∀ a, a ∈ o → p a) (h : ∀ {x}, p x →  q x ):
  (o.attach.map (fun x => Subtype.mk x.val (h (f x.val x.2)))).isSome := by
  fail_if_success rw [map_attach_eq_attachWith_no_abstract] -- does not rewrite, LHS hard to unify?
  rw [map_attach_eq_attachWith_with_abstract]
  · sorry
  · solve_by_elim

So abstracting over proofs in theorems makes them more applicable, which seems a good thing in general, but of course breaks things. Sigh.

---

More breakage with abstracted proofs:

protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
  Fin.ext <| by rw [mul_def, mul_def]; unfold mul_def.proof_1; rw [Nat.mul_comm]

Without unfolding the abstracted proof we get

tactic 'rewrite' failed, motive is not type correct:
  fun _a => ↑⟨_a % n, mul_def.proof_1 a b⟩ = ↑⟨↑b * ↑a % n, mul_def.proof_1 b a⟩
Error: application type mismatch
  ⟨_a % n, mul_def.proof_1 a b⟩
argument
  mul_def.proof_1 a b
has type
  ↑a * ↑b % n < n : Prop
but is expected to have type
  _a % n < n : Prop

which is not surprising: With a and b occurring separately now they don’t get abstracted by kabstract and rewriting fails. This seems harder to work-around or fix than the more-lemmas-rewrite-with-simp issue.

For reference:

theorem Fin.mul_def.proof_1 : ∀ {n : Nat} (a b : Fin n), ↑a * ↑b % n < n :=
fun {n} a b => Nat.mod_lt (↑a * ↑b) (Fin.pos a)

---

Another breakage was already fixed in #7355