From 0cc9d7a43de73af086597c48e2ff427f31fef4f3 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 8 Mar 2023 14:03:30 -0800
Subject: [PATCH] fix: do not reverse subgoals of local instances

---
 src/Lean/Meta/SynthInstance.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index b118e83eac..f25300cf98 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -312,14 +312,11 @@ private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInst
 def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) (inst : Expr) : MetaM SubgoalsResult := do
   let instType ← inferType inst
   let result ← getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType
-  match inst.getAppFn with
-  | Expr.const constName _ =>
+  if let .const constName _ := inst.getAppFn then
     let env ← getEnv
     if hasInferTCGoalsRLAttribute env constName then
       return result
-    else
-      return { result with subgoals := result.subgoals.reverse }
-  | _ => return result
+  return { result with subgoals := result.subgoals.reverse }
 
 /--
   Try to synthesize metavariable `mvar` using the instance `inst`.