Lean 4: section variables used only inside `by` blocks are not included in a def

If a variable (h : P) hypothesis is used only inside a tactic proof in a def's body, for example a membership proof passed to MonoidHom.codRestrict, Lean 4 does not include it as an argument. Callers then fail with 'Application type mismatch: argument h has type Prop but is expected to have type ↥N', because the next explicit argument is shifted. Lemmas that mention the def together with h in their statements then break in confusing ways. Fix: write the hypothesis as an explicit binder on the def itself, or use include h. The unusedSectionVars linter doesn't warn about this.