[Merged by Bors] - chore: replace haveI/letI with have/let in tactics when the goal is a prop

[thorimur]

Using haveI/letI for instances in proofs is a holdover from Lean 3, and is unnecessary in Lean 4. As explained by @Vierkantor on Zulip here:

Historical note: a lot of the haveI/letI usage is a remnant of Lean 3 times, where the I stood for Instances: the old versions of the have/let tactics would not add the new variable to the list of available instances, and you'd need haveI/letI to force an update to the instance cache and make them visible. In our modern Lean 4 age, basic have/let already make the instance available and I instead only stands for Inline. But the old haveI got ported to the new haveI and so there is a bit of a superstition that we have to keep using haveI and letI for instances.

(Note that inlining can change IR for compiled defs, so we don't change those.)

Try-this statements produced by #41657; applied mechanically by running scripts/runSkimmer.sh.

Then, Mathlib.CategoryTheory.Galois.Basic was fixed up manually: it turned out that the haveI's triggering the linter were completely unnecessary, which might be why universe issues came about when the linter suggested turning them into haves.

Cleaning up term-mode haveI/letI is left for another PR.

Co-authored-by: @JovanGerb

---

[github-actions]

PR summary e381f6e76d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

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 e381f6e).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e381f6e76d
Reference commit 8ccb214159

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).

[thorimur]

!bench

[leanprover-radar]

Benchmark results for e381f6e against 8ccb214 are in. No significant results found. @thorimur

• ✅ build//instructions: -71.2G (-0.05%)

Medium changes (1🟥)

• 🟥 build/module/Mathlib.FieldTheory.PurelyInseparable.PerfectClosure//instructions: +4.3G (+13.27%)

[JovanGerb]

Thanks for making the PR!

[grunweg]

Thanks for the PR! Can you edit the PR description to say why this change was made? (You can copy from Anne's comment on the Zulip thread.)
bors d+

[mathlib-bors]

✌️ thorimur can now approve this pull request until 2026-07-28 10:14 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[thorimur]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Test and lint
• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job