NNG- adding valid assumptions to prove a goal

Stream: new members

[D A L]

image.png
Image shows where I'm at in Level 8 in ≤ world. I would like to add the (true) assumption that d ≤ succ d, then use le_trans to prove that succ d_n ≤ d ≤ succ d = succ d_n ≤ succ d, completing the goal. Is there a way to do this in Lean?

[David Ledvinka]

The way to add a true assumption in full lean is "have" which is greyed out. However your idea still works if you just use apply le_trans (succ d_n) d (This will create the subgoal for you)

[D A L]

David Ledvinka said:

The way to add a true assumption in full lean is "have" which is greyed out. However your idea still works if you just use apply le_trans (succ d_n) d (This will create the subgoal for you)

That did work, thank you. Although to be honest, I don't understand how. I wanted to add the subgoal d ≤ succ d, but that command doesn't mention succ d. Does it know to add that because there is d at the end? And why does succ d_n have to be in parentheses?

[Philippe Duchon]

The parentheses are necessary because otherwise the high priority of function evaluation (the function being le_trans) would make this be parsed as apply (((le_trans succ) d_n) d).

For the first question: le_trans is transitivity of the order: from naturals a, b, c, a proof of a≤b and a proof of b≤c, it produces a proof of a≤c. You need to provide the value of b, because Lean cannot infer it from your goal.

Since your goal is to prove succ d_n ≤ succ d, then a can only be succ d_n and c can only be succ d, but there is no similar way to guess what b should be; so you need to provide the first two parameters and then Lean figures what the remaining ones should be (and can ask for the two intermediate inequalities, which become new goals).

[David Ledvinka]

I should mention that the same proof actually works if you erase the two parameters I provided and just put apply le_trans but then your goal in the next step is the confusing: succ d_n ≤ ?succ.inl.h.succ.y because as mentioned by Philippe Lean doesn't know what b should be. However if you write exact h1 at this step it can then infer b. I left this out of my original answer since its a little more advanced.