Goal metavariable seems to be assigned twice?

Stream: lean4

[Matěj Kripner]

My understanding of tactic proofs is that goalsAfter of a tactic are equal to goalsBefore of the following tactic. However, this proof Mathlib.Algebra.CubicDiscriminant seems to defy that:

private theorem coeffs : (∀ n > 3, P.toPoly.coeff n = 0) ∧ P.toPoly.coeff 3 = P.a ∧
    P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d := by
  simp only [toPoly, coeff_add, coeff_C, coeff_C_mul_X, coeff_C_mul_X_pow]
  norm_num
  intro n hn
  repeat' rw [if_neg]
  any_goals omega
  repeat' rw [zero_add]

When I open the corresponding file in VS Code and put the cursor after any_goals omega, "No goals" is displayed and the proof seems to be finished. However, when I put the cursor before repeat' rw [zero_add], there is one open goal (⊢ 0 + 0 + 0 + 0 = 0). Also, if I remove the last tactic, there is a warning "unsolved goals".
The same weirdness can be seen when looking at the goal metavariables - the metavariable ⊢ 0 + 0 + 0 + 0 = 0 is the goalBefore of both omega and rw [zero_add], so it seems to be assigned twice!

Can you please show me what I'm missing?

[Adam Topaz]

I think those zeros are in R, not in Nat.

[Adam Topaz]

so it's not surprising that omega can't close the goal.

[Adam Topaz]

I think the No Goals you see when you put the cursor at the end of any_goals omega is telling you that omega solved the goal that it worked on.

[Adam Topaz]

Here's a MWE:

example (p : Prop) : p ∧ (1 + 2 = 3) := by
  constructor
  any_goals omega
  sorry

It may have something to do with omega itself, because we don't get the same behavior in

example (p q : Prop) (hp : p) : p ∧ q := by
  constructor
  any_goals assumption
  sorry