From ff149122e25a0be27547b738a1f14b270dff55ee Mon Sep 17 00:00:00 2001
From: damiano <adomani@gmail.com>
Date: Fri, 12 Apr 2024 19:06:06 +0000
Subject: [PATCH] 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 |  2 +-
 test/abel.lean           | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Abel.lean b/Mathlib/Tactic/Abel.lean
index f47d2a7a814e6..79a9820672460 100644
--- a/Mathlib/Tactic/Abel.lean
+++ b/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))
diff --git a/test/abel.lean b/test/abel.lean
index 3a191ef22e61f..7338aa7490d9f 100644
--- a/test/abel.lean
+++ b/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
 -/