feat(tactic/congr): additions to the congr' tactic (#3936)
This PR gives a way to apply `ext` after `congr'`.
`congr' 3 with x y : 2` is a new notation for `congr' 3; ext x y : 2`.
New tactic `rcongr` that recursively keeps applying `congr'` and `ext`.
Move `congr'` and every tactic depending on it from `tactic/interactive` to a new file `tactic/congr`.
The original `tactic.interactive.congr'` is now best called as `tactic.congr'`.
Other than the tactics `congr'` and `rcongr` no tactics have been (essentially) changed.
