[Merged by Bors] - perf(linear_algebra): speed up graded_algebra instances

[alreadydone]

Reduce elaboration of graded_algebra in:

• exterior_algebra.graded_algebra from ~20s to 3s-
• tensor_algebra.graded_algebra from 7s+ to 2s-
• clifford_algebra.graded_algebra from 14s+ to 4s-

(These numbers were before lift_ι and lift_ι_eq were extracted from exterior_algebra.graded_algebra and lift_ι_eq was extracted from clifford_algebra.graded_algebra in #12182.)

Fix timeout reported on Zulip

Also shorten the statements of the first two without reducing clarity (I think).

---

[eric-wieser]

This conflicts fairly heavily with 32b08ef#diff-f20af6ffdb513b03c216be5b63e2095d959f0350cb7b8ed495eb450f2965f11c

[eric-wieser]

I think your approach is cleaner, if it doesn't time out.

[alreadydone]

The extracted lift_ι_eq (and lift_ι in the case of clifford_algebra) are still slow so the same fixes apply. Should I inline them again, or just speed up the extracted def/lemmas?

[alreadydone]

I removed a few by apply that are not statistically significant; the remaining ones were tested to shaves off 0.x seconds ~ several seconds each.

[kmill]

Thanks!

bors r+

(You might consider writing some kind of library note about using by apply for performance. I'm not sure how important that is, though, since this might just be a short-term fix until these tricks become potentially irrelevant with Lean 4.)

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests