Variables not included automatically (tpil)

Stream: general

[Ben Selfridge]

Hello -- I'm going through some lean intro materials again as a refresher, and I'm having trouble with something in here: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html

In particular, the following doesn't work for me:

variable (a b c d e : Nat)
variable (h1 : a = b)
variable (h2 : b = c + 1)
variable (h3 : c = d)
variable (h4 : e = 1 + d)

theorem T : a = e :=
  calc
    a = b      := h1
    _ = c + 1  := h2
    _ = d + 1  := congrArg Nat.succ h3
    _ = 1 + d  := Nat.add_comm d 1
    _ = e      := Eq.symm h4

I get unknown identifier errors for every variable besides a and e, even though I've declared all the other variables alongside those two. Does anyone have any ideas? Is this a bug in the documentation?

[Ruben Van de Velde]

The hn variables are no longer included automatically, and that means the other variables are also excluded. You can write include h1 h2 h3 h4 in before theorem

[Notification Bot]

2 messages were moved here from #general > R golfing by Ruben Van de Velde.