You only type in the reasons, not the results. Lean computes the result for you. Otherwise, if you do all the work yourself, you wouldn't need Lean :-)
If it shows you something of the form `X=X` like `37=37`, you then type in `rfl` to assert that they are equal by the reflective property which completes the proof.
You only type in the reasons, not the results. Lean computes the result for you. Otherwise, if you do all the work yourself, you wouldn't need Lean :-)
I still am completely lost. Can you give me the answer so I can see what input is supposed to look like?
In my head I want to solve it with 37=37, x=x and q=q. And then run rfl
If it shows you something of the form `X=X` like `37=37`, you then type in `rfl` to assert that they are equal by the reflective property which completes the proof.
You can just type in `rfl` to assert that `37 = 37` (or anything of the form `X = X`).
I typed in rfl and hit execute and nothing happened (it added a line above but did not say I solved anything)