editing PRs

Stream: mathlib4

[Jireh Loreaux]

Do we just want to make it standard practice while porting that reviewers should / can just go ahead and edit PRs (at least when they are sure of what they are doing and not asking a question)? It might cut down on review turn-around time significantly. Perhaps we would require them to at least explain the changes they've made briefly in a comment. Thoughts?