fix: apply

src/Lean/Meta/Tactic/Apply.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Util.FindMVar
 import Lean.Meta.ExprDefEq
 import Lean.Meta.SynthInstance
+import Lean.Meta.CollectMVars
 import Lean.Meta.Tactic.Util
 
 namespace Lean
@@ -87,10 +88,14 @@ withMVarContext mvarId $ do
   (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType (some numArgs);
   unlessM (isDefEq eType targetType) $ throwApplyError mvarId eType targetType;
   postprocessAppMVars `apply mvarId newMVars binderInfos;
+  e ← instantiateMVars e;
   assignExprMVar mvarId (mkAppN e newMVars);
   newMVars ← newMVars.filterM $ fun mvar => not <$> isExprMVarAssigned mvar.mvarId!;
+  otherMVarIds ← getMVarsNoDelayed e;
   -- TODO: add option `ApplyNewGoals` and implement other orders
-  reorderNonDependentFirst newMVars
+  newMVarIds ← reorderNonDependentFirst newMVars;
+  let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId;
+  pure $ newMVarIds ++ otherMVarIds.toList
 
 end Meta
 end Lean

tests/lean/run/new_frontend2.lean

@@ -26,6 +26,22 @@ by {
   exact rfl
 }
 
-def ex : {α : Type} → {a b c : α} → a = b → b = c → a = c :=
+def ex1 : {α : Type} → {a b c : α} → a = b → b = c → a = c :=
 @(by intro α a b c h₁ h₂;
      exact Eq.trans h₁ h₂)
+
+def f1 (x : Nat) : Nat := by
+apply (· + ?hole);
+exact 1;
+case hole => exact x
+
+theorem ex2 (x : Nat) : f1 x = 1 + x :=
+rfl
+
+def f2 (x : Nat) : Nat := by
+apply Nat.add _;
+exact 1;
+exact x
+
+theorem ex3 (x : Nat) : f2 x = x + 1 :=
+rfl