feat: add the haveILetI linter, flagging haveI/letI in tactic proofs …

[kbuzzard]

…of propositions

The tactics haveI and letI differ from have and let only in that they inline the given value into the term being constructed (in current core they are literally have +zeta and let +zeta, sharing a single elaborator). In a tactic proof of a proposition this difference is invisible by proof irrelevance, so have/let should be used instead.

The linter walks the InfoTree and flags each user-written haveI/letI tactic whose main goal is a proposition, checked by running Meta.isProp on the goal type in the recorded metavariable/local context. Term-mode haveI/letI and macro-generated syntax are not flagged (documented TODO). The option linter.style.haveILetI is off by default; mathlib currently contains ~2,300 sites the linter would flag.

---

This PR is 100% vibe-coded with Claude Fable and I can not vouch for any of it.

[github-actions]

PR summary 69ed66568a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all
There are 7255 files with changed transitive imports taking up over 325477 characters: this is too many to display!
You can run this locally from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

---

Declarations diff (regex)

+ candidates
+ haveILetILinter
+ mainGoalIsProp
+ oneAsSubtype
+ replacement?
+ zero

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 69ed665).

• +1 new declarations
• −0 removed declarations

+Mathlib.Linter.linter.style.haveILetI

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 69ed66568a
Reference commit 32ea179db3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

I believe we had such a linter in the past. @adomani Did you write that one? Do you remember if that was worth it?

[adomani]

I don't remember this linter, but I do remember writing one to detect haves that should be lets (or the other way round, or both ways!).

[adomani]

This seems a bit awkward: can't you use directly getRange?? (Talking to Claude here!)