An nth_simp_rw tactic would be great

Stream: maths

[Mark Andrew Gerads]

image.png
In this situation, I want to replace the outer cexp with its Taylor series, but not the inner cexp.
nth_rewrite is a great tactic, but does not work in this case. simp_rw replaces both instances of cexp.
I thus propose the creation of a tactic that rewrites inside binders like simp_rw, but only rewrites the nth instance like nth_rewrite.

[Scott Morrison]

Provide arguments for cexp in the simp_rw, or use conv.

[Scott Morrison]

Implementing nth_simp_rw would be very awkward, in a way that it isn't for rw.