From bd42c396d71097b100852aa1f25d3759f76edfe0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Mon, 20 May 2024 14:19:10 -0700
Subject: [PATCH] chore: Code cleanup

---
 Pantograph/Expr.lean    | 5 ++---
 Pantograph/Library.lean | 3 +--
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean
index 8f890e3..63331af 100644
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@@ -70,11 +70,10 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
         let pending ← mvarIdPending.withContext do
           let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
           --IO.println s!"{padding}├Pre: {inner}"
-          let r := (← Expr.abstractM inner fvars).instantiateRev args
-          pure r
+          pure <| (← inner.abstractM fvars).instantiateRev args
 
         -- Tail arguments
-        let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray)
+        let result := mkAppRange pending fvars.size args.size args
         --IO.println s!"{padding}├MD {result}"
         return .done result
       else
diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean
index e0625e8..d3df45f 100644
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@@ -212,11 +212,10 @@ inductive TacticExecute where
 def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult :=
   runTermElabM do
     state.restoreElabM
-    let tactic := match tacticExecute with
+    state.execute goalId $ match tacticExecute with
       | .congruenceArg => Tactic.congruenceArg
       | .congruenceFun => Tactic.congruenceFun
       | .congruence => Tactic.congruence
-    state.execute goalId tactic