chore(*): remove `subst` when not necessary (#13453)
Where possible, this replaces `subst` with `obtain rfl` (which is equivalent to `have` and then `subst`, golfing a line).
This also tidies some non-terminal `simp`s.
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
