Comment by sn9

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.