Commit 2022-07-18 17:22 9c7a7cca

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