Commit 2023-08-27 12:05 9a9e31c7

feat: congr(...) congruence quotations and port congrm tactic (#2544) Adds a term elaborator for congr(...) "congruence quotations". For example, if hf : f = f' and hx : x = x', then we have congr($hf $x) : f x = f' x'. This supports the functions having implicit arguments, and it has support for subsingleton instance arguments. So for example, if s t : Set X are sets with Fintype instances and h : s = t then congr(Fintype.card $h) : Fintype.card s = Fintype.card t works. Ports the congrm tactic as a convenient frontend for applying a congruence quotation to the goal. Holes are turned into congruence holes. For example, congrm 1 + ?_ uses congr(1 + $(?_)). Placeholders (_) do not turn into congruence holes; that's not to say they have to be identical on the LHS and RHS, but congrm itself is responsible for finding a congruence lemma for such arguments.