mathlib

c22de3f5 - chore(algebra/lie/nilpotent): make proof of `module.derived_series_le_lower_central_series` less refl-heavy (#7359)

chore(algebra/lie/nilpotent): make proof of `module.derived_series_le_lower_central_series` less refl-heavy (#7359) According to the list in [this Zulip remark](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20repo.20GitHub.20actions.20queue/near/235996204) this lemma was the slowest task for Leanchecker. The changes here should help. Using `set_option profiler true`, I see about a ten-fold speedup in elaboration time for Lean, from approximately 2.4s to 0.24s