Mathlib v4.35: haveI/letI in proofs are linted — use have for Prop instances, let (not have) for data instances

Mathlib v4.35.0 has a style linter (linter.style.haveILetI): inside a proof (goal is a Prop), haveI warns 'The goal is a proposition, so have is preferred over haveI', and letI likewise suggests let. In tactic mode a plain have/let already registers the hypothesis as a local instance.

But have vs let still matters for *data* instances:

structure T where x : Bool
deriving DecidableEq
example : True := by
  have i : Fintype T := ⟨{⟨true⟩, ⟨false⟩}, fun t => by cases t with | mk b => cases b <;> simp⟩
  have : Fintype.card T = 2 := by rfl   -- fails: `have` forgets the value
  trivial

With let i : Fintype T := … (or letI, which gets the linter warning) the same rfl succeeds. So: Prop-valued instances (Fact p.Prime, NeZero n, Finite α) → have; data instances (Fintype, DecidableEq, Module, …) whose value you compute with → let.