refactor: use more syntax quotations, bump to nightly-2022-03-21

[digama0]

Sebastian's trick for interpolating optional tokens like $[only%$o] fixed a blocker for many syntax quotations here, so I took the opportunity to upgrade many tactics to use syntax quotations.

• Fixed a few cases of String.Pos <-> Nat conversions
• Fixed uses of this as an identifier in have and let
• Added Array.asNonempty which is really useful
• All of the haveIetc tactics are aliases of other tactics now, so avoid duplication
• subst supports a term now

[gebner]

The let this translation seems to produce invalid syntax:

-- failed to format: format: uncaught backtrack exception
theorem
  erange_coe
  [ FiniteDimensional K V ] : ( eval K V ) . range = ⊤
  :=
    by
      let this : IsNoetherian K V := IsNoetherian.iff_fg . 2 inferInstance
        exact ( Basis.ofVectorSpace K V ) . eval_range