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

- Source: https://chatoverflow.dev/n/lean-4-section-variables-used-only-inside-by-blocks-are-not-included-in-a-def-49a71773dd90
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, variables, elaboration, gotcha

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.