From d6f0c324c31d81191e91ef4294f55fbd66190b85 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 13 Jan 2025 18:25:30 -0800
Subject: [PATCH] chore: display E-matching theorems in `goalToMessageData`
 (#6635)

This PR includes the activated E-matching theorems and their patterns in
`goalToMessageData`
---
 src/Lean/Meta/Tactic/Grind/PP.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Grind/PP.lean b/src/Lean/Meta/Tactic/Grind/PP.lean
index 536c2ec613..c39f06f594 100644
--- a/src/Lean/Meta/Tactic/Grind/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/PP.lean
@@ -99,10 +99,23 @@ private def ppEqcs (goal : Goal) : MetaM (Array MessageData) := do
      result := result.push <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
    return result
 
+private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
+  let m := m!"{← thm.origin.pp}\n{← inferType thm.proof}\npatterns: {thm.patterns.map ppPattern}"
+  return .trace { cls := `thm } m #[]
+
+private def ppActiveTheorems (goal : Goal) : MetaM MessageData := do
+  let m ← goal.thms.toArray.mapM ppEMatchTheorem
+  let m := m ++ (← goal.newThms.toArray.mapM ppEMatchTheorem)
+  if m.isEmpty then
+    return ""
+  else
+    return .trace { cls := `ematch } "E-matching" m
+
 def goalToMessageData (goal : Goal) : MetaM MessageData := goal.mvarId.withContext do
   let mut m : Array MessageData := #[.ofGoal goal.mvarId]
   m := m.push <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop
   m := m ++ (← ppEqcs goal)
+  m := m.push (← ppActiveTheorems goal)
   addMessageContextFull <| MessageData.joinSep m.toList ""
 
 def goalsToMessageData (goals : List Goal) : MetaM MessageData :=