fix: mdata in abel (#12084)

PR inspired by "automated bugs" (#12054).

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/automated.20bugs/near/432861117)

Mathlib/Tactic/Abel.lean

@@ -473,7 +473,7 @@ open Elab.Tactic Parser.Tactic
 /-- Use `abel_nf` to rewrite the main goal. -/
 def abelNFTarget (s : IO.Ref AtomM.State) (cfg : AbelNF.Config) : TacticM Unit := withMainContext do
   let goal ← getMainGoal
-  let tgt ← instantiateMVars (← goal.getType)
+  let tgt ← withReducible goal.getType'
   let r ← abelNFCore s cfg tgt
   if r.expr.isConstOf ``True then
     goal.assign (← mkOfEqTrue (← r.getProof))

test/abel.lean

@@ -51,6 +51,16 @@ example [AddCommGroup α] (a b c : α) :
     left; abel1
   right; trivial
 
+/-- `MyTrue` should be opaque to `abel`. -/
+private def MyTrue := True
+
+/--
+error: abel_nf made no progress
+-/
+#guard_msgs in
+example : MyTrue := by
+  abel_nf
+
 -- `abel!` should see through terms that are definitionally equal,
 def id' (x : α) := x
 example [AddCommGroup α] (a b : α) : a + b - b - id' a = 0 := by
@@ -73,6 +83,11 @@ example [AddCommGroup α] (x y z : α) : y = x + z - (x - y + z) := by
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/abel.20bug.3F/near/368707560
 example [AddCommGroup α] (a b s : α) : -b + (s - a) = s - b - a := by abel_nf
 
+-- inspired by automated testing
+example : True := by
+  have := 0
+  abel_nf
+
 /--
 error: abel_nf made no progress
 -/