mathlib

41eb9587 - feat({tactic + test}/congrm, logic/basic): `congrm = congr + pattern-match` (#14153)

feat({tactic + test}/congrm, logic/basic): `congrm = congr + pattern-match` (#14153) This PR defines a tactic `congrm`. If the goal is an equality, where the sides are "almost" equal, then calling `congrm <expr_with_mvars_for_differences>` will produce goals for each place where the given expression has metavariables and will try to close the goal assuming all equalities have been proven. For instance, ``` example {a b : ℕ} (h : a = b) : (λ y : ℕ, ∀ z, a + a = z) = (λ x, ∀ z, b + a = z) := begin congrm λ x, ∀ w, _ + a = w, exact h, end ``` works. [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> Co-authored-by: Gabriel Ebner <gebner@gebner.org>