feat: upstream congr! from Mathlib

[kim-em]

This is a preliminary step to upstreaming convert.

We should later think about combining this with the standard congr.

There is still a builtin problem here, that you can not use congr! (config := ...) without import Lean.Meta.Tactic.Congr!. We need to move the config structure into e.g. Init/MetaTypes.lean, and then an update-stage0, but I haven't got it to work.

This is stacked on top of #3671 and #3672, and I'll wait for those to merge.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8d2adf521d2b7636347a5b01bfe473bf0fcfaf31 --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 04:03:05)

[kmill]

Oh wow, I wasn't expecting to see that congr! was being upstreamed! That should be fine, but I've been thinking of simplifying it now that we've now seen it in action for a while in mathlib. (And I'm looking forward to congr one day being able to do everything congr! can do!)

By the way, I have an open PR to add that LawfulBEq instances are equal: leanprover-community/mathlib4#11179

[kim-em]

Oh wow, I wasn't expecting to see that congr! was being upstreamed! That should be fine, but I've been thinking of simplifying it now that we've now seen it in action for a while in mathlib. (And I'm looking forward to congr one day being able to do everything congr! can do!)

By the way, I have an open PR to add that LawfulBEq instances are equal: leanprover-community/mathlib4#11179

@kmill, I don't think it is super urgent, so if you think there is good reason to delay moving it to allow for a refactor, I think we can do that. I'm happy with moving it as is and updating later, however.

[kmill]

I don't have any good reason to delay merging it, and I'm not sure when I'd get around to refactoring it, so carrying on with upstreaming seems fine to me. (Thanks!)

[nomeata]

Is there any hope that we can have a single congr tactic in lean, so that users don't have to learn about the difference? What would happen if this congr! were the only one?

Ah, I see in the comments above that this is the plan, or at least the hope.

[kim-em]

We decided not to proceed at this point. @kmill is refactoring the Mathlib implementation in the meantime.