linter.fugue.setNotLet

set x := e exists to abstract a term e that already occurs in the goal — it rewrites every occurrence to x and hands back x = e. When e occurs nowhere, set rewrites nothing: the goal is unchanged, and a proof-local definition with no abstraction to do is a let.

The check is exactly that: the goal type before the set equals the goal type after. let m := Nat.find hall for a fresh m, set m := Nat.find hall where Nat.find hall is in the goal — the first trips this, the second does not.

set … with h is left alone: the equation is doing work, and let (eq := h) (the replacement) binds it in the opposite direction, which is not a mechanical swap.