Lean features used without being presented

[arademaker]

From the ledger in STYLE-CODE.md. IntroCS is not among these — its use of
unpresented Lean is the constraint's one accepted exception, recorded in
DEVIATIONS.md and announced in the chapter itself.

• native_decide — CSwL/Morphology/SwedishPlural.lean:69, :72, inside
  solutions, absent from IntroL's tactic table. It closes a goal by
  compiling and running it, trusting the compiler rather than the kernel: a
  materially different promise from decide, and a reader who meets it
  without being told will draw the wrong conclusion about what a Lean proof is
  worth. There is an explanation at :63-66 — rfl and decide stall on
  swedishVowels.contains noun.back because the internal String blocks
  reduction — but it is a Lean comment, inside the solution, in Portuguese, so
  it reaches neither the student nor the English code-comment rule. Either
  promote it to prose or reformulate so decide closes.
• trivial — one term-level use, CSwL/Sets.lean:507. Give it a line or
  replace it when that chapter is revised.
• injection — two uses in CSwL/Logic/PL.lean. It belongs to that
  chapter, which states constructor injectivity with it; part of the PL.lean
  work, not separate.
• instance : Fintype Player — CSwL/Sets.lean:606, the only instance in
  the book that is not a ToString. Finset and Fintype themselves are now
  presented (:591), and so is Setoid (:844); what is left is this one
  declaration, whose shape the reader has not seen.