From 77b9dbf9a98fec8cd75b2aa91d4ca75de9549057 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 May 2021 17:15:04 -0700
Subject: [PATCH] feat: add `casesRec`

---
 src/Lean/Meta/Tactic/Cases.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index 8a2a51dad4..d542681580 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -321,6 +321,28 @@ end Cases
 def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array AltVarNames := #[]) : MetaM (Array CasesSubgoal) :=
   Cases.cases mvarId majorFVarId givenNames
 
+def casesRec (mvarId : MVarId) (p : LocalDecl → MetaM Bool) : MetaM (List MVarId) :=
+  saturate mvarId fun mvarId =>
+    withMVarContext mvarId do
+      for localDecl in (← getLCtx) do
+        if (← p localDecl) then
+          try
+            let r ← cases mvarId localDecl.fvarId
+            return some <| r.toList.map (·.mvarId)
+          catch _ =>
+            pure ()
+      return none
+
+def casesAnd (mvarId : MVarId) : MetaM MVarId := do
+  let mvarIds ← casesRec mvarId fun localDecl => return (← instantiateMVars localDecl.type).isAppOfArity ``And 2
+  exactlyOne mvarIds
+
+def substEqs (mvarId : MVarId) : MetaM MVarId := do
+  let mvarIds ← casesRec mvarId fun localDecl => do
+    let type ← instantiateMVars localDecl.type
+    return type.isEq || type.isHEq
+  exactlyOne mvarIds
+
 builtin_initialize registerTraceClass `Meta.Tactic.cases
 
 end Lean.Meta