chore(lean): clear the 106 linter warnings from the build

[barghouthi]

Why

Every lake build replayed cached diagnostics for 15 modules. Nothing was actually recompiling — Replayed means Lake found the cache valid and re-printed the warnings stored from the last real compile — but 106 warnings scrolling past on every invocation reads like a rebuild.

Before:

15 Replayed   0 Built   0 Compiling

plus 106 warnings.

After:

Build completed successfully (5267 jobs).

lake exe tzap-lean is likewise silent before the program's own output.

What changed

15 files, +88/−96. No sorry, no change to any statement — only to the tactic scripts proving them.

fix	count
unused simp args dropped from simp/simp only lists	76
simpa … using e → simp […] where simp closed it alone	6
unreferenced binders _-prefixed (hC, hrange×3, hd)	5
dead first alternatives / never-executed tactics removed	5
tac1 <;> tac2 → single-goal form	4

Three places the linter's suggestion was wrong

Each of these was applied, failed the build, and then fixed a different way:

1. SemanticsCheck — try (rw [pow_two]; exact hsq.symm) (×5). The linter flags exact hsq.symm as doing nothing, and it never does close a goal — but it is load-bearing: it makes the surrounding try roll back when rw [pow_two] leaves a goal behind. Rewriting to try rw [pow_two] keeps the rewrite and broke two goals. Deleting the line outright works, because the try (rw [pow_two, hsq]) / try rw [hsq] / try ring cascade below it picks those goals up.

2. SemanticsCheck:1184 and CnotMinProof:234 — <;> → ;. Fails with No goals to be solved: the left tactic closes all goals in one branch, and ; errors on zero goals where <;> no-ops. Used all_goals for the follow-up instead.

Two notes for anyone repeating this pass:

• The unused-simp-arg linter tests each argument individually, so removing several from one call can break it. SemanticsCheck.lean:98 needed map_one, map_neg checked together.
• Where a list emptied out, simp [] was normalized to simp. Merge.lean:142 legitimately keeps simp only [] at hb' — both its args were unused, but the call still reduces hb'.

Verification

lake build exits 0 with zero errors and zero warnings; a second invocation is a clean no-op in ~1.3s.