mathlib

0783742a - chore(*): more assumptions to lemmas that are removable (#13364)

chore(*): more assumptions to lemmas that are removable (#13364) This time I look at assumptions that are actually provable by simp from the earlier assumptions (fortunately there are only a couple of these), and one more from the review of #13316 that was slightly too nontrivial to be found automatically.