∀ (s : String) (p : s.Pos) (res : Lean.Name),
  Lean.Name.demangleAux.nameStart✝ s p res =
    if h : p = s.endPos then res
    else
      let ch := p.get h;
      let p_1 := p.next h;
      if ch.isDigit = true then
        if h_1 : ch = '0' ∧ ∃ (h : p_1 ≠ s.endPos), p_1.get h = '0' then Lean.Name.demangleAux✝ s (p_1.next ⋯) res "" 0
        else Lean.Name.demangleAux.decodeNum✝ s p_1 res (ch.val - 48).toNat
      else
        if ch = '_' then Lean.Name.demangleAux✝¹ s p_1 res "" 1
        else Lean.Name.demangleAux✝² s p_1 res (String.singleton ch) 0