fix the fix

Author: Kha

Mathlib/Tactic/Linarith/Frontend.lean

@@ -516,15 +516,14 @@ elab_rules : tactic
     commitIfNoEx do liftMetaFinishingTactic <| Linarith.linarith o.isSome args.toList cfg
 
 private meta partial def minimize (cfg : Linarith.LinarithConfig) (st : Tactic.SavedState)
-    (hs : List Expr) (i : Nat) : TacticM (List Expr) := do
-  let g ← getMainGoal
+    (g : MVarId) (hs : List Expr) (i : Nat) : TacticM (List Expr) := do
   if _h : i < hs.length then
     let rest := hs.eraseIdx i
     st.restore
     try
       let _ ← Linarith.linarith true rest cfg g
-      minimize cfg st rest i
-    catch _ => minimize cfg st hs (i+1)
+      minimize cfg st g rest i
+    catch _ => minimize cfg st g hs (i+1)
   else
     return hs
 
@@ -543,7 +542,7 @@ elab_rules : tactic
             throwError "linarith? currently only supports named hypothesis, not terms"
           let used ←
             if cfg.minimize then
-              minimize cfg st used₀ 0
+              minimize cfg st g used₀ 0
             else
               pure used₀
           st.restore