Refer to simplified definition from the sidebar

Stream: lean4

[Amrit M Joseph]

image.png

I am in the middle of an assignment. The last line on this is a simple Nat.succ_le_succ. But how do I refer to that statement in the code?

[Kevin Buzzard]

How have you ended up with inaccessible variables? Did you name two different things a?