`rw` and `simp` do not invoke tactics specified in auto-params

Here is mwe provide by Jireh Loreaux.

theorem foo (m : Nat) (h : m.succ = 1 := by assumption) : m.succ = 1 := h

theorem foo' (m : Nat) (h : m.succ = 1) : m.succ = 1 := h

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo'] -- succeeds, leaving the goal `⊢ m.succ = n`
  exact h

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo _] -- succeeds, the autoParam fills the proof obligation

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  rw [foo]
  /-
  tactic 'assumption' failed

  m✝: Nat
  h: Nat.succ m✝ = 1
  m: Nat
  ⊢ Nat.succ m = 1
  -/

example (m : Nat) (h : m.succ = 1) : m.succ = 1 := by
  simp [foo _] -- succeeds, the autoParam fills the proof obligation

example (m : Nat) (h : m.succ = 1) : 1 + m.succ = 2 := by
  simp [foo] -- simp made no progress

The main obstacle is that to execute tactics we need to be in TacticM, but simp and rw implemented using MetaM. We had to address a similar issue for implementing custom discharge tactics for simp: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Simp.lean#L37

Start with the custom simp discharge-tactic implementation cited in src/Lean/Elab/Tactic/Simp.lean around line 37, then trace how rw and simp handle auto-params. The examples in the issue should execute the tactic supplied by the auto-param, and the final simp example should make progress.