feat(Mathlib/Tactic/Setm): implement setm tactic

[grhkm21]

This is my first time doing metaprogramming in Lean 4, please provide feedback when you have them :)

The setm tactic, which stands for set + matching, matches a given expression with the goal and introduces new local hypotheses for the named holes specified. One of the best usage is for rearrangement proofs. As a simple example,

example : (1 + 1) + (4 * 3) - (1 + 1) = (3 * 4 : Rat) := by
  setm ?A + ?B - ?A = (?C : Rat)
  rw [show ∀ A B, A + B - A = B by intro A B ; ring_nf ]
  apply Rat.mul_comm

One can imagine replacing the three term expression with a 7 term algebraic expression.

This was developed with tons of help from Zulip, especially from Thomas. Thanks!

TODO:

• Support setm ... at ... syntax, see example 1 below
• Write docs
• Use withNewMCtxDepth
• Rename the intermediate MVars, see example 2 below
• Use elabTermWithHolesPostponing in conjunction with Term.synthesizeSyntheticMVarsNoPostPoning after isDefEq to handle instances

Example 1:

/- Usage with `using` and `at` keywords -/
example (h1 : 1 + 1 = 3) (h2 : 1 + 3 = 5) (h3 : 2 + 2 = 5) : true := by
  setm ?A + _ = (?B : Nat) using h2 at h1 h2 h3
  guard_hyp A := 1
  guard_hyp B := 5
  guard_hyp h1 : A + A = 3
  guard_hyp h2 : A + 3 = B
  guard_hyp h3 : 2 + 2 = B
  trivial

Example 2:

/- Test reusing named holes -/
example (h : b + a = c) : a + b = c := by
  /- setm 1-/
  setm ?A + ?B = (_ : Nat)
  guard_hyp A := a
  guard_hyp B := b
  /- clean up -/
  unfold_let A B
  clear hA hB A B
  /- setm 2 -/
  rewrite [Nat.add_comm]
  setm ?A + ?B = (_ : Nat) at h ⊢
  guard_hyp A := b
  guard_hyp B := a
  exact h

Co-authored-by: Jireh Loreaux loreaujy@gmail.com