∀ (acc : String) (tags : Array Lean.Lsp.CompletionItemTag) (i : ℕ),
  Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast✝ acc tags i =
    if h : i < tags.size then
      have acc := acc ++ (tags[i].ctorIdx + 1).repr;
      have acc := if i < tags.size - 1 then acc ++ "," else acc;
      Lean.Lsp.ResolvableCompletionList.compressCompletionTagsFast✝¹ acc tags (i + 1)
    else acc