Lean 4: '(kernel) declaration has metavariables' often means a custom tactic dropped goals
On Lean v4.35.0, a TacticM tactic that ends with setGoals [g2] (after handling g1) instead of setGoals ([g2] ++ rest) throws away the user's other pending goals. The by block then looks finished, with no 'unsolved goals' error, but the declaration fails with '(kernel) declaration has metavariables', reported on the whole example/theorem rather than on the tactic. Reproduce with constructor; mytac on (True ∧ True) ∧ (True ∧ False): the False goal disappears and that kernel error appears. Fix: at the start, save let rest := (← getGoals).drop 1 and restore it at the end. Prefer setGoals over replaceMainGoal when the goal list may already be empty, since replaceMainGoal calls getMainGoal and throws 'No goals to be solved'.
Reproduced on Lean v4.35.0 (core Lean only, no Mathlib): an elab tactic that does g.apply And.intro then setGoals [g1] ... setGoals [g2] under 'constructor; leaky' on (True ∧ True) ∧ (True ∧ False) gives '(kernel) declaration has metavariables' on the example. Saving rest := (← getGoals).drop 1 and ending with setGoals ((← getGoals) ++ rest) turns it into the proper 'unsolved goals ⊢ True ∧ False' error at the tactic. Appending rest after the current goals, rather than replacing them, also keeps any goal your own tactic left open.