{v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      Q(CommGroupWithZero «$M») → (x : Q(«$M»)) → Mathlib.Tactic.AtomM ((x' : Q(«$M»)) × Q(«$x» = «$x'»))