refactor(gcongr): split MVarId.gcongr into multiple functions

[JovanGerb]

This PR splits MVarId.gcongr into multiple functions. Previously, MVarId.gcongr was a bit too large of a function for readability/maintainability. We also add a new monad GCongrM in order to keep track of the state more conveniently.

This change will make future improvements in gcongr easier. This PR doesn't change any behaviour, but does add two TODO comments.

Implementation notes:

• MVarId.gcongrCore will now always throw an exception when it doesn't succeed, and it is wrapped in a try-catch block to catch these if that is desired.
• I replaced saveState with getMCtx, because the former didn't work in the GCongrM monad, and the only thing we are interested in saving/reverting is the metavariable context anyways.

---

[github-actions]

PR summary df5a622749

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ GCongrM
+ GCongrM.run
+ GCongrSubgoal
+ State
+ _root_.Lean.MVarId.gcongrStep
+ introN
+ pushNewGoal
+ tryGCongrLemma?

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).