From 319940da77a6fd684ef5cfe366dcfc988363e195 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 17 Apr 2024 12:41:34 -0700
Subject: [PATCH] feat: make anonymous instance names not include proofs
 (#3934)

---
 src/Lean/Elab/DeclNameGen.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean
index 8d94e64353..2995bf4b22 100644
--- a/src/Lean/Elab/DeclNameGen.lean
+++ b/src/Lean/Elab/DeclNameGen.lean
@@ -51,6 +51,8 @@ Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned.
 -/
 private partial def winnowExpr (e : Expr) : MetaM Expr := do
   let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr := checkCache e fun _ => do
+    if ← isProof e then
+      return .bvar 0
     match e with
     | .app .. =>
       if let some e' ← getParentProjArg e then