fix(tactic/congr): fix trivial congr/convert (#6011)
Now `convert` will prove reflexivity goals even at the top level, before
applying any congruence rules. Under the interpretation of the depth
argument as the number of nested congruence rules applied, we allow
proofs by assumption or reflexivity to work even at depth 0.
Also fixes a bug where
```lean
example {α} (a b : α) : a = b := by congr'
```
would succeed, because `apply proof_irrel` will unify the universe
metavariable in the type of `α` to `Prop`, causing surprising behavior.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
