Variables not imported

Stream: mathlib4

[María Inés de Frutos Fernández]

After updating Mathlib in our project with @Antoine Chambert-Loir , we are having issues with some variables that are used in the proof but not in the statement not being imported. Antoine is having the same problem in his main Mathlib branch, which he just updated. Here is a mwe:

import Mathlib.Algebra.Order.Ring.Nat

variable {n : ℕ} (hn : 1 < n)

theorem test :  0 < n := lt_trans zero_lt_one hn -- unknown identifier 'hn'

[Ruben Van de Velde]

Yep, use include hn in before the theorem, or don't use variable for it

[Antoine Chambert-Loir]

Is it a new rule?

[Sebastian Ullrich]

https://github.com/leanprover/lean4/releases/tag/v4.11.0

[Antoine Chambert-Loir]

Thanks!

[Antoine Chambert-Loir]

From a stylistic point of view, what is preferred for mathlib, using variable… and include… in or adding the variable each time?

[Matthew Ballard]

The latter.