chore(docs/tutorial): change category declarations (#3220)
change category declarations to match syntax in recent commit (i.e. no more explicit typeclass naming), delete unnecessary "include" lines as they are no longer needed for Lean to include the typeclass, update tutorial text to explain new syntax
Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>
