feat(gcongr): use mdata instead of template (#30739)

This PR changes the implementation of `gcongr` patterns. Instead of carrying around another expression of the same shape, we put a metadata annotation in the actual goal, in order to keep track of where we want to apply more `gcongr` lemmas.

This makes the implementation neater, and this is a necessary step towards supporting more operations in `gcongr`, such as those from the `congr!` tactic.

This also means that the pattern given to the `gcongr` tactic is checked to be fully correct. This helped fix one pattern in mathlib that was `∑ _ : α, ?_`, but should have been `∑ _ : β, ?_`.

Another change that this PR makes is that if the goal relation is `a → b`, then we run reducible `whnf` on `a` and `b` before getting the two sides of the relation. This means that `x > y` is reduced to `y < x`. This is needed because this refactor now is keeping track of which side is which side, and to do this consistently, we need `x > y` to be swapped into `y < x`.

Author: JovanGerb

Mathlib/NumberTheory/SiegelsLemma.lean

@@ -75,7 +75,7 @@ private lemma image_T_subset_S [DecidableEq α] [DecidableEq β] (v) (hv : v ∈
   refine ⟨fun i ↦ ?_, fun i ↦ ?_⟩
   all_goals
     simp only [mul_neg]
-    gcongr ∑ _ : α, ?_ with j _ -- Get rid of sums
+    gcongr ∑ _ : β, ?_ with j _ -- Get rid of sums
     rw [← mul_comm (v j)] -- Move A i j to the right of the products
     rcases le_total 0 (A i j) with hsign | hsign-- We have to distinguish cases: we have now 4 goals
   · rw [negPart_eq_zero.2 hsign]

Mathlib/Order/Basic.lean

@@ -195,8 +195,6 @@ theorem forall_ge_iff_le : (∀ ⦃c⦄, a ≤ c → b ≤ c) ↔ b ≤ a :=
 
 namespace Mathlib.Tactic.GCongr
 
-@[gcongr] theorem gt_imp_gt (h₁ : a ≤ c) (h₂ : d ≤ b) : a > b → c > d := lt_imp_lt_of_le_of_le h₂ h₁
-
 /-- See if the term is `a < b` and the goal is `a ≤ b`. -/
 @[gcongr_forward] def exactLeOfLt : ForwardExt where
   eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``le_of_lt #[h])