Commit 2025-02-02 13:52 794c8dd9

perf: fix some slow declarations (#21323) This PR fixes some slow declarations, by

• changing the proof slightly so that unification is happier
• giving more arguments in a rw theorem
• replacing a slow set with let.
• explicitly supplying an autoparam proof, or adding the result to the context to help the autoparam.
• fixing a type so that a slow erw can become a less slow rw.
• replacing ‹Ring R› with (‹Ring R›:), which forces the expression to be fully elaborated immediately, instead of temporarily turning into a synthetic metavariable.
• reordering the instances in a spread construction of an instance (so that the ancestor that is represented as a subobject field comes first). See also #21030 for another example of this. To find most of these, I took a look at the declarations that use at least 100000 heartbeats (i.e. at least half of the default maximum).