linter.fugue.byInArg

A tactic proof passed as an argument is a step with no name and no goal displayed. Two replacements: a term when one exists (often the side condition is a hypothesis up to defeq), else a ?_ and the next line — exact f (g (by tac)) becomes refine f (g ?_) then tac.

LEAN_STYLE.md calls this "too common to mechanize", so the linter ships off — flip it on (set_option linter.fugue.byInArg true in …) for a deliberate one-file sweep.

Covers both application arguments (f (by …)) and anonymous-constructor components (⟨…, by …, …⟩) — the latter is more common and takes longer to work off.

The solely-assumption case is linter.fugue.byAssumption's; this linter leaves it alone.