From 3367f0b06aefe4a30921cdfa8a9bef2abafaedce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 8 Feb 2022 12:53:09 -0800
Subject: [PATCH] feat: use `splitTarget?` when proving equation theorems for
 recursive definitions

---
 src/Lean/Elab/PreDefinition/Structural/Eqns.lean | 2 ++
 src/Lean/Elab/PreDefinition/WF/Eqns.lean         | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
index 6ba313d665..f902d4af2b 100644
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -50,6 +50,8 @@ where
           go mvarId
         else if let some mvarIds ← casesOnStuckLHS? mvarId then
           mvarIds.forM go
+        else if let some mvarIds ← splitTarget? mvarId then
+          mvarIds.forM go
         else
           throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"
 
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index 1b91804101..b82d44bfa5 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -57,6 +57,8 @@ where
       | TacticResultCNM.noChange =>
         if let some mvarIds ← casesOnStuckLHS? mvarId then
           mvarIds.forM go
+        else if let some mvarIds ← splitTarget? mvarId then
+          mvarIds.forM go
         else
           throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"