feat: add tech debt counter for disabled varHead simp warnings

This PR adds a counter for `set_option warning.simp.varHead false`
occurrences to the weekly tech debt report.

The `warning.simp.varHead` option silences a warning introduced in Lean
about simp lemmas whose LHS has a metavariable as its head. Places where
this warning is silenced are tech debt we want to track over time.

Prompted by discussion on
leanprover-community/mathlib4-nightly-testing#209
which adds several `set_option warning.simp.varHead false in` uses.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: kim-em

scripts/reporting/technical-debt-metrics.sh

@@ -132,6 +132,8 @@ doubleDeprecs="$(git grep -A2 -- "set_option linter.deprecated false" -- ":^Math
 
 printf '%s|disabled deprecation lints\n' "$(( deprecs - doubleDeprecs ))"
 
+printf '%s|%s\n' "$({ git grep -c 'set_option warning.simp.varHead false' -- Mathlib Archive Counterexamples || true; } | awk -F: 'BEGIN{s=0}{s+=$2} END{print s}')" "disabled varHead simp warnings"
+
 printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nolint entries"
 printf '%s|%s\n' "$(grep -c 'tacticDocs' scripts/nolints.json)" "undocumented tactics"
 # We count the number of large files, making sure to avoid counting the test file `MathlibTest/Lint.lean`.