mathlib3

9c7a7cca - feat(tactic/congrm): add "function underscores" to `congrm` (#14532)

feat(tactic/congrm): add "function underscores" to `congrm` (#14532) This PR introduces further functionality to tactic `congrm`. It is now possible to use "function underscores": for instance, ``` example {a b c d e f g h : ℕ} (ae : a = e) (bf : b = f) (cg : c = g) (dh : d = h) : (a + b) * (c - d.succ) = (e + f) * (g - h.succ) := by congrm _₂ (_₂ _ _) (_₂ _ (_₁ _)); assumption ``` works. Each `_₂` is interpreted as the correct operation, `*, +, -`. I implemented `_ᵢ` for `i ∈ {1,2,3,4}`. It is easy to extend it further, in case this is desired. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/variant.20syntax.20for.20.60congr'.60) Co-authored-by: Gabriel Ebner <gebner@gebner.org>