Update Lean, mathlib, and Rocq

[stepchowfun]

This updates the proof toolchains:

• Lean: v4.34.0 → v4.34.1 (patch release)
• mathlib: v4.34.0 → v4.34.1. Its transitive dependencies (batteries, aesop, Qq, etc.) are unchanged at this tag, so only mathlib's entry in lake-manifest.json changes.
• rocq-core: 9.2.0 → 9.3.0
• rocq-stdlib: 9.1.0 → 9.2.0 (it supports Rocq 9.1–9.3)

Rocq 9.3 adds or upgrades several warnings in the default category. Since _RocqProject passes -w +default, they are errors here, so this PR fixes them:

• missing-proof-command: two Goals in tutorial/lesson5_consistency.v now start with Proof.
• at-level-200-changed: the tutorial's exists notation in tutorial/lesson3_logic.v now uses at level 10, x binder, p at level 200 (dropping right associativity), which matches how Rocq 9.3's prelude declares it.
• non-boolean-if: the sumbool guards (name_eq, eq_nat_dec) in stlc and system_f now use if ... is left _ then ... else .... This elaborates to the same match. Arms that exceeded the 79-column limit are wrapped.

I verified the Rocq build locally with rocq/rocq-prover:9.3 (9.3+rc1, stdlib 9.2.0): all 60 files compile with no warnings.

rocq makefile now prints a deprecation warning about omitting --rocq-package. It doesn't fail the build, so this PR leaves it alone.

The copyright year in LICENSE.md is already current, and all GitHub Actions are already at their latest versions.

Status: Ready