suggested by @alreadydone here #6806 (comment)

Thanks!
I can find some similar lemmas in mathlib that are simp lemmas (e.g. Polynomial.hermite_succ, Cardinal.aleph'_succ, aleph_succ, beth_succ) and some that are not (GeneralizedContinuedFraction.convergents_succ, Sensitivity.f_succ_apply, Function.iterate_succ_apply), and I think it's reasonable to remove simp here.

maintainer merge

🚀 Pull request has been placed on the maintainer queue by alreadydone.

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style

Thanks! I can find some similar lemmas in mathlib that are simp lemmas (e.g. Polynomial.hermite_succ, Cardinal.aleph'_succ, aleph_succ, beth_succ) and some that are not (GeneralizedContinuedFraction.convergents_succ, Sensitivity.f_succ_apply, Function.iterate_succ_apply), and I think it's reasonable to remove simp here.

@alreadydone
Perhaps also
Function.iterate_succ does not need to be simp?

Probably? If you search for it you'll see lots of use of the primed version Function.iterate_succ' (or Function.iterate_succ_apply') which transforms the LHS in another way. But I must admit I'm not familiar with rationales to mark a lemma @[simp] or not, as I seldom at any simp attribute in my work at all ...