diff --git a/src/Lean/Meta/Diagnostics.lean b/src/Lean/Meta/Diagnostics.lean
index 2cce90c99327..d1b9c832edb7 100644
--- a/src/Lean/Meta/Diagnostics.lean
+++ b/src/Lean/Meta/Diagnostics.lean
@@ -85,6 +85,9 @@ def appendSection (m : Array MessageData) (cls : Name) (header : String) (s : Di
 /-- Logs diagnostics and resets the counters -/
 def reportDiag : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
+    -- Diagnostic output may reference private declarations (e.g. `_match_*`,
+    -- `_sparseCasesOn_*`) that are not visible in exporting mode (issue #13581).
+    withoutExporting do
     let unfoldCounter := (← get).diag.unfoldCounter
     let unfoldDefault ← mkDiagSummaryForUnfolded unfoldCounter
     let unfoldInstance ← mkDiagSummaryForUnfolded unfoldCounter (instances := true)
diff --git a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
index ed0746a2811d..cfd3477548dd 100644
--- a/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
+++ b/src/Lean/Meta/Tactic/Simp/Diagnostics.lean
@@ -67,6 +67,9 @@ def mkDiagMessages (diag : Simp.Diagnostics) : MetaM (Array MessageData) := do
 
 def reportDiag (diag : Simp.Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
+    -- Diagnostic output may reference private declarations that are not visible
+    -- in exporting mode (issue #13581).
+    withoutExporting do
     let m ← mkDiagMessages diag
     unless m.isEmpty do
       logInfo <| .trace { cls := `simp, collapsed := false } "Diagnostics" m
diff --git a/tests/elab/13581.lean b/tests/elab/13581.lean
new file mode 100644
index 000000000000..5bfbcbd784cb
--- /dev/null
+++ b/tests/elab/13581.lean
@@ -0,0 +1,15 @@
+-- https://github.com/leanprover/lean4/issues/13581
+-- Reporting `diagnostics` must not crash on private match/sparseCasesOn helpers
+-- in module mode under a `public section`.
+module
+
+public section
+
+def onlyTrue : Bool → Bool
+  | true => true
+  | x    => x
+
+#guard_msgs (drop trace) in
+set_option diagnostics true in
+set_option diagnostics.threshold 0 in
+example : onlyTrue true = true := rfl