diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 9373bd7329a2..a18da60cbde1 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -18,13 +18,6 @@ def DefKind.isTheorem : DefKind → Bool
   | .theorem => true
   | _        => false
 
-def DefKind.isDefOrAbbrevOrOpaque : DefKind → Bool
-  | .def      => true
-  | .instance => true
-  | .opaque   => true
-  | .abbrev   => true
-  | _         => false
-
 def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index ccb1af447708..f075fe7f3ccb 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -863,7 +863,7 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
   letRecClosures.foldlM (init := preDefs) fun preDefs c => do
     let type  := Closure.mkForall c.localDecls c.toLift.type
     let value := Closure.mkLambda c.localDecls c.toLift.val
-    let kind ← if kind.isDefOrAbbrevOrOpaque then
+    let kind ← if kind matches .def | .instance | .opaque | .abbrev then
       -- Convert any proof let recs inside a `def` to `theorem` kind
       withLCtx c.toLift.lctx c.toLift.localInstances do
         return if (← inferType c.toLift.type).isProp then .theorem else kind