feat: haveI/letI tactic linter (leanprover-community#41657)

JovanGerb · JovanGerb · commit 30696563acb0 · 2026-07-29T20:08:20.000Z
This PR implements a variation on the linter that was written by Claude in leanprover-community#41562. It suggest to use `have`/`let` instead of `haveI`/`letI` whenever the goal is a proposition. See also https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/surprising.20have.2FhaveI.20kernel.20phenomenon/with/609718493
diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean
@@ -34,7 +34,7 @@ namespace Imo2008Q3
 
 theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (hp_gt_20 : p > 20) :
     ∃ n : ℕ, p ∣ n ^ 2 + 1 ∧ (p : ℝ) > 2 * n + sqrt (2 * n) := by
-  haveI := Fact.mk hpp
+  have := Fact.mk hpp
   have hp_mod_4_ne_3 : p % 4 ≠ 3 := by linarith [show p % 4 = 1 from hp_mod_4_eq_1]
   obtain ⟨y, hy⟩ := ZMod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3
   let m := ZMod.valMinAbs y
diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean
@@ -275,7 +275,7 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by
     rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _)
       hwbtw.mem_affineSpan]
     exact cfg.PQ_parallel_AB.direction_eq
-  haveI := someOrientation V
+  have := someOrientation V
   have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by
     rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B]
     rw [Set.pair_comm, Set.insert_comm]
@@ -389,7 +389,7 @@ end Oriented
 
 
 theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ←
     affineIndependent_iff_not_collinear_set]
   have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by
@@ -515,13 +515,13 @@ end Oriented
 
 
 theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA,
     Set.pair_comm, Set.insert_comm, Set.pair_comm]
   exact cfg.not_collinear_ABC
 
 theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by
-  haveI := someOrientation V
+  have := someOrientation V
   rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁,
     Set.pair_comm]
   exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear
diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean
@@ -315,9 +315,9 @@ theorem ballot_problem' :
     rw [div_self]
     exact Nat.cast_add_one_ne_zero p
   · intro q p qp h₁ h₂
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite p (q + 1)) (countedSequence_nonempty _ _)
-    haveI := isProbabilityMeasure_uniformOn
+    have := isProbabilityMeasure_uniformOn
       (countedSequence_finite (p + 1) q) (countedSequence_nonempty _ _)
     have h₃ : 0 < p + 1 + (q + 1) := Nat.add_pos_left (Nat.succ_pos _) _
     rw [← uniformOn_add_compl_eq {l : List ℤ | l.headI = 1} _ (countedSequence_finite _ _),
@@ -344,7 +344,7 @@ theorem ballot_problem' :
 theorem ballot_problem :
     ∀ q p, q < p → uniformOn (countedSequence p q) staysPositive = (p - q) / (p + q) := by
   intro q p qp
-  haveI :=
+  have :=
     isProbabilityMeasure_uniformOn (countedSequence_finite p q) (countedSequence_nonempty _ _)
   have :
     (uniformOn (countedSequence p q) staysPositive).toReal =
diff --git a/Archive/Wiedijk100Theorems/CubingACube.lean b/Archive/Wiedijk100Theorems/CubingACube.lean
@@ -378,7 +378,7 @@ variable (h v)
   direction will intersect one of the neighbouring cubes on the same boundary as `mi`. -/
 theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈ _) j := by
   let i := mi h v; have hi : i ∈ bcubes cs c := mi_mem_bcubes
-  haveI := h.nontrivial_fin
+  have := h.nontrivial_fin
   rcases exists_ne j with ⟨j', hj'⟩
   intro hj
   rcases smallest_onBoundary hj with ⟨x, ⟨hx, h2x⟩, h3x⟩
diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
@@ -250,7 +250,7 @@ theorem false_of_three_le_degree (hd : G.IsRegularOfDegree d) (h : 3 ≤ d) : Fa
   have p_dvd_d_pred := (ZMod.natCast_eq_zero_iff _ _).mpr (d - 1).minFac_dvd
   have dpos : 1 ≤ d := by lia
   have d_cast : ↑(d - 1) = (d : ℤ) - 1 := by norm_cast
-  haveI : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
+  have : Fact p.Prime := ⟨Nat.minFac_prime (by lia)⟩
   have hp2 : 2 ≤ p := (Fact.out (p := p.Prime)).two_le
   have dmod : (d : ZMod p) = 1 := by
     rw [← Nat.succ_pred_eq_of_pos dpos, Nat.succ_eq_add_one, Nat.pred_eq_sub_one]
diff --git a/Counterexamples/CliffordAlgebraNotInjective.lean b/Counterexamples/CliffordAlgebraNotInjective.lean
@@ -155,7 +155,7 @@ theorem sq_map_add_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a
 
 theorem sq_map_sub_char_two {ι R : Type*} [CommRing R] [CharP R 2] (i : ι) (a b : ι → R) :
     sq i (a - b) = sq i a - sq i b := by
-  haveI : Nonempty ι := ⟨i⟩
+  have : Nonempty ι := ⟨i⟩
   rw [CharTwo.sub_eq_add, CharTwo.sub_eq_add, sq_map_add_char_two]
 
 /-- The quadratic form (metric) is just Euclidean -/
diff --git a/Counterexamples/Phillips.lean b/Counterexamples/Phillips.lean
@@ -248,7 +248,7 @@ theorem exists_discrete_support_nonpos (f : BoundedAdditiveMeasure α) :
   -- convenient to formalize the inductive construction.
   let A : Set (Set α) := {t | t.Countable}
   let empty : A := ⟨∅, countable_empty⟩
-  haveI : Nonempty A := ⟨empty⟩
+  have : Nonempty A := ⟨empty⟩
   -- given a countable set `s`, one can find a set `t` in its complement with measure close to
   -- maximal.
   have : ∀ s : A, ∃ t : A, ∀ u : A, f (↑u \ ↑s) ≤ 2 * f (↑t \ ↑s) := by
diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean
@@ -68,7 +68,7 @@ theorem isOpen_Ici (a : ℝₗ) : IsOpen (Ici a) :=
 
 theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := by
   rw [TopologicalSpace.nhds_generateFrom]
-  haveI : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
+  have : Nonempty { x // x ≤ a } := Set.nonempty_Iic_subtype
   have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by
     refine (IsLeast.isGLB ?_).iInf_eq
     exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_mem_range.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩
@@ -313,7 +313,7 @@ theorem not_separatedNhds_rat_irrational_antidiag :
 /-- Topology on the Sorgenfrey line is not metrizable. -/
 theorem not_metrizableSpace : ¬MetrizableSpace ℝₗ := by
   intro
-  letI := metrizableSpaceMetric ℝₗ
+  let := metrizableSpaceMetric ℝₗ
   exact not_normalSpace_prod inferInstance
 
 /-- Topology on the Sorgenfrey line is not second countable. -/
diff --git a/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean b/Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean
@@ -244,8 +244,8 @@ example : ¬UniqueProds ℕ := by
 
 /-- Some Types that do not have `UniqueSums`. -/
 example (n : ℕ) (n2 : 2 ≤ n) : ¬UniqueSums (ZMod n) := by
-  haveI : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩
-  haveI : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne'
+  have : Fintype (ZMod n) := @ZMod.fintype n ⟨(zero_lt_two.trans_le n2).ne'⟩
+  have : Nontrivial (ZMod n) := CharP.nontrivial_of_char_ne_one (one_lt_two.trans_le n2).ne'
   rintro ⟨h⟩
   refine not_not.mpr (h Finset.univ_nonempty Finset.univ_nonempty) ?_
   suffices ∀ x y : ZMod n, ∃ x' y' : ZMod n, x' + y' = x + y ∧ (x' = x → ¬y' = y) by
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -7421,6 +7421,7 @@ public import Mathlib.Tactic.Linter.FindDeprecations
 public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.GlobalAttributeIn
 public import Mathlib.Tactic.Linter.HashCommandLinter
+public import Mathlib.Tactic.Linter.HaveILetI
 public import Mathlib.Tactic.Linter.HaveLetLinter
 public import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.Linter.Lint
diff --git a/Mathlib/Analysis/Convex/Side.lean b/Mathlib/Analysis/Convex/Side.lean
@@ -882,7 +882,7 @@ alias isPreconnected_setOf_wOppSide := isPreconnected_setOfPred_wOppSide
 theorem isConnected_setOfPred_sOppSide {s : AffineSubspace ℝ P} {x : P} (hx : x ∉ s)
     (h : (s : Set P).Nonempty) : IsConnected { y | s.SOppSide x y } := by
   obtain ⟨p, hp⟩ := h
-  haveI : Nonempty s := ⟨⟨p, hp⟩⟩
+  have : Nonempty s := ⟨⟨p, hp⟩⟩
   rw [setOfPred_sOppSide_eq_image2 hx hp, ← Set.image_prod]
   refine (isConnected_Iio.prod (isConnected_iff_connectedSpace.2 ?_)).image _
     ((continuous_fst.smul continuous_const).vadd continuous_snd).continuousOn
diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean
@@ -73,7 +73,7 @@ open Manifold IsManifold
 lemma isImmersionOfComplement_subtypeVal_Icc :
     IsImmersionOfComplement Unit (𝓡∂ 1) 𝓘(ℝ) n (fun (z : Icc x y) ↦ (z : ℝ)) := by
   intro z
-  letI φ₀ := ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
+  let φ₀ := ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
   let φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ :=
     φ₀.trans (PiLp.equivOfUnique 2 ℝ (fun (_ : Fin 1) ↦ ℝ))
   by_cases hz : ↑z < y
diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean
@@ -81,7 +81,7 @@ variable {M}
 
 theorem commProb_eq_one_iff [h : Nonempty M] : commProb M = 1 ↔ IsMulCommutative M := by
   classical
-  haveI := Fintype.ofFinite M
+  have := Fintype.ofFinite M
   rw [commProb, ← Set.coe_ofPred, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
   rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
     set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean
@@ -13,6 +13,7 @@ public import Mathlib.Tactic.Linter.DocString
 public import Mathlib.Tactic.Linter.EmptyLine
 public import Mathlib.Tactic.Linter.GlobalAttributeIn
 public import Mathlib.Tactic.Linter.HashCommandLinter
+public import Mathlib.Tactic.Linter.HaveILetI
 public import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.Multigoal
diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean
@@ -146,7 +146,7 @@ theorem of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Dis
 theorem of_biUnion {ι : Type*} {s : Set ι} {f : ι → Set α} (hs : s.Countable)
     (hd : s.Pairwise (Disjoint on f)) (h : ∀ b ∈ s, MeasurableSet (f b)) :
     v (⋃ b ∈ s, f b) = ∑' p : s, v (f p) := by
-  haveI := hs.toEncodable
+  have := hs.toEncodable
   rw [biUnion_eq_iUnion]
   apply of_disjoint_iUnion
   · exact fun x ↦ h x x.2
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -191,6 +191,7 @@ public import Mathlib.Tactic.Linter.FindDeprecations
 public import Mathlib.Tactic.Linter.FlexibleLinter
 public import Mathlib.Tactic.Linter.GlobalAttributeIn
 public import Mathlib.Tactic.Linter.HashCommandLinter
+public import Mathlib.Tactic.Linter.HaveILetI
 public import Mathlib.Tactic.Linter.HaveLetLinter
 public import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.Linter.Lint
diff --git a/Mathlib/Tactic/Linter/HaveILetI.lean b/Mathlib/Tactic/Linter/HaveILetI.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Jovan Gerbscheid. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jovan Gerbscheid
+-/
+module
+
+public meta import Lean.Meta.Hint
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+public import Mathlib.Tactic.Linter.Header  -- shake: keep
+
+/-!
+# The `haveI`/`letI` linter
+
+The tactics `haveI` and `letI` differ from `have` and `let` only in that they inline
+the given value into the term being constructed, instead of binding it with a
+`have`/`let` binder. (In Lean 3, `haveI`/`letI` were additionally needed to make the new
+hypothesis available to instance resolution; in Lean 4, `have` and `let` register local
+instances themselves, so inlining is the only remaining difference.)
+
+Inside the proof of a proposition this difference is invisible: proofs are irrelevant,
+so nothing can depend on whether a value was inlined into the proof term. Hence
+`haveI`/`letI` are never needed in tactic proofs of propositions, and `have`/`let`
+should be used instead.
+
+This linter flags every use of the `haveI` or `letI` tactic whose main goal is a
+proposition.
+
+TODO:
+* also lint the term-mode `haveI`/`letI`
+-/
+
+meta section
+
+open Lean Elab Meta Parser.Term Tactic Linter
+
+namespace Mathlib.Linter.HaveILetI
+
+/-- The `haveILetI` linter flags uses of the `haveI` or `letI` tactic in a proof of a
+proposition. Since proofs are irrelevant, the value-inlining behaviour of `haveI`/`letI`
+can have no effect there, and `have`/`let` should be used instead. -/
+public register_option linter.style.haveILetI : Bool := {
+  defValue := true
+  descr := "enable the `haveILetI` linter"
+}
+
+/-- Run the `haveI` tactic, with a try this suggestion when the goal is a `Prop`. -/
+def runHaveI (tk : Syntax) (c : TSyntax ``letConfig) (d : TSyntax ``letDecl) : TacticM Unit := do
+  evalTactic (← `(tactic| haveI $c:letConfig $d:letDecl))
+  if getLinterValue linter.style.haveILetI (← getLinterOptions) then
+    withMainContext do
+    if ← isProp (← getMainTarget) then
+      let suggs ← Hint.mkSuggestionsMessage #[{toTryThisSuggestion := "have"}] tk none false
+      logLint linter.style.haveILetI (← getRef) m!"Try this: {suggs}\n\n\
+        The goal is a proposition, so `have` is preferred over `haveI`.\n\
+        The difference between `have` and `haveI` is that `haveI` inlines the value.\n\
+        But this is not relevant for proofs because of proof irrelevance."
+
+@[tactic_alt Parser.Tactic.tacticHaveI__]
+elab (priority := high) tk:"haveI" c:letConfig d:letDecl : tactic => runHaveI tk c d
+
+/-- Run the `letI` tactic, with a try this suggestion when the goal is a `Prop`. -/
+def runLetI (tk : Syntax) (c : TSyntax ``letConfig) (d : TSyntax ``letDecl) : TacticM Unit := do
+  evalTactic (← `(tactic| letI $c:letConfig $d:letDecl))
+  if getLinterValue linter.style.haveILetI (← getLinterOptions) then
+    withMainContext do
+    if ← isProp (← getMainTarget) then
+      let suggs ← Hint.mkSuggestionsMessage #[{toTryThisSuggestion := "let"}] tk none false
+      logLint linter.style.haveILetI (← getRef) m!"Try this: {suggs}\n\n\
+        The goal is a proposition, so `let` is preferred over `letI`.\n\
+        The difference between `let` and `letI` is that `letI` inlines the value.\n\
+        But this is not relevant for proofs because of proof irrelevance."
+
+@[tactic_alt Parser.Tactic.tacticLetI__]
+elab (priority := high) tk:"letI" c:letConfig d:letDecl : tactic => runLetI tk c d
+
+end Mathlib.Linter.HaveILetI
diff --git a/MathlibTest/InstanceDiamonds.lean b/MathlibTest/InstanceDiamonds.lean
@@ -154,7 +154,7 @@ the domain is a group. -/
 example {k : Type _} [Semiring k] [Nontrivial kˣ] :
     (Finsupp.comapSMul : SMul kˣ (kˣ →₀ k)) ≠ Finsupp.smulZeroClass.toSMul := by
   obtain ⟨u : kˣ, hu⟩ := exists_ne (1 : kˣ)
-  haveI : Nontrivial k := Units.val_injective.nontrivial
+  have : Nontrivial k := Units.val_injective.nontrivial
   intro h
   simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, DFunLike.ext_iff] at h
   replace h := h u (Finsupp.single 1 1) u
diff --git a/MathlibTest/Linter/HaveILetI.lean b/MathlibTest/Linter/HaveILetI.lean
@@ -0,0 +1,28 @@
+module
+
+public import Mathlib.Tactic.Linter.HaveILetI
+
+/--
+warning: Try this: ⏎
+  haveI̵
+
+The goal is a proposition, so `have` is preferred over `haveI`.
+The difference between `have` and `haveI` is that `haveI` inlines the value.
+But this is not relevant for proofs because of proof irrelevance.
+
+Note: This linter can be disabled with `set_option linter.style.haveILetI false`
+---
+warning: Try this: ⏎
+  letI̵
+
+The goal is a proposition, so `let` is preferred over `letI`.
+The difference between `let` and `letI` is that `letI` inlines the value.
+But this is not relevant for proofs because of proof irrelevance.
+
+Note: This linter can be disabled with `set_option linter.style.haveILetI false`
+-/
+#guard_msgs in
+example : True := by
+  haveI : True := trivial
+  letI : True := trivial
+  trivial
diff --git a/MathlibTest/Tactic/ITauto.lean b/MathlibTest/Tactic/ITauto.lean
@@ -60,9 +60,9 @@ set_option linter.unusedVariables false in
 set_option linter.unusedTactic false in
 -- failure tests
 example (p q r : Prop) : True := by
-  haveI : p ∨ ¬p := by (fail_if_success itauto); sorry
-  clear this; haveI : ¬(p ↔ q) → ¬p → q := by (fail_if_success itauto); sorry
-  clear this; haveI : ¬(p ↔ q) → (r ↔ q) → (p ↔ ¬r) := by (fail_if_success itauto); sorry
+  have : p ∨ ¬p := by (fail_if_success itauto); grind
+  clear this; have : ¬(p ↔ q) → ¬p → q := by (fail_if_success itauto); grind
+  clear this; have : ¬(p ↔ q) → (r ↔ q) → (p ↔ ¬r) := by (fail_if_success itauto); grind
   trivial
 
 example (P : Nat → Prop) (n : Nat)
diff --git a/MathlibTest/TransImports.lean b/MathlibTest/TransImports.lean
@@ -3,8 +3,8 @@ import Mathlib.Util.TransImports
 /--
 info: 'MathlibTest.TransImports' has at most 2000 transitive imports
 
-2 starting with "Mathlib.Tactic.Linter.H":
-[Mathlib.Tactic.Linter.HashCommandLinter, Mathlib.Tactic.Linter.Header]
+3 starting with "Mathlib.Tactic.Linter.H":
+[Mathlib.Tactic.Linter.HashCommandLinter, Mathlib.Tactic.Linter.HaveILetI, Mathlib.Tactic.Linter.Header]
 -/
 #guard_msgs in
 #trans_imports "Mathlib.Tactic.Linter.H" at_most 2000
