Commit 2022-07-15 13:03 1a424e18

chore(number_theory/modular): add missing lemmas to squeeze simps (#15351) I was running into some timeouts in exists_smul_mem_fd when making some other changes; this extracts some simp calls to standalone lemmas. These lemmas don't have particularly fast proofs either, but the statements are much simpler so will be easier to speed up in future if we need to. Simp-normal form in this file seems to aggressively unfold to matrices, so we can't mark these new lemmas simp. At some point the simp lemmas for modular forms might want to be revisited.