Commit 2024-05-17 01:34 8bf14d13

chore: remove an unused congr lemma (#12567) This removes a congr lemma which is unused in Mathlib, and on Lean master can trigger exponential behaviour. (edit: in fact, the remaining congr lemma here still triggers exponential behaviour, just with a smaller exponent than with both) Seems safest to just get it out of the way, and I'll separately report the linear --> exponential change on master, as it may affect other congr lemmas which are harder to simply remove.