`Zero ℕ` instance breaks `acyclic` tactic

import Mathlib

inductive Foo
| mk (t s : Foo)

-- `Lean.MVarId.acyclic` failed:
example (h: Foo.mk s s = s): False := nomatch h  -- missing cases

-- because of `simp_arith` can't solve this goal:
example: sizeOf s < sizeOf (Foo.mk s s) := by simp_arith  -- unsolved goals

-- problem arises there:
example {n: Nat}: Zero.zero ≤ n := by simp  -- simp made no progress

Start with the three minimal Lean examples in the issue, especially the Zero.zero ≤ n goal and the uses of Lean.MVarId.acyclic and simp_arith. Reproduce the failures in a small file, then trace the relevant Zero ℕ instance and confirm that simplification, arithmetic, and acyclicity work without unsolved goals.