Remove two unnecessary rws

[darabos]

Removes two unnecessary rw applications.

---

Sorry about the possibly pointless PR. I was working on something else and hit these. I think with some more effort I could find and remove all the unnecessary rw rules in Mathlib. Would that be useful? Or is it better to keep these?

Thanks!

[Vierkantor]

Hi, thanks for the pull request! Unfortunately due to technical limitations we can't review pull requests from a fork: could you please push directly to a new branch of the leanprover-community/mathlib4 repository and reopen the PR from there? I have sent you a contributor invitation so you have push access. Feel free to assign the new PR to me, then it's on my todo list.

[urkud]

I'll try to manually hit "Approve and run" button to see what happens.

[darabos]

Hi, thanks for the pull request! Unfortunately due to technical limitations we can't review pull requests from a fork: could you please push directly to a new branch of the leanprover-community/mathlib4 repository and reopen the PR from there? I have sent you a contributor invitation so you have push access. Feel free to assign the new PR to me, then it's on my todo list.

Sorry, I took too long and the invitation expired. Could you please re-send it? Thank you! (I'll also fix the conflicts.)

[Vierkantor]

Invite resent!

[darabos]

Invite resent!

Got it, thanks! I've reposted this from an in-repository branch as #10704. That PR has all the unnecessary rules that I found.