fix(logic/basic): remove `noncomputable lemma` (#10292)
It's been three years since this was discussed according to the zulip archive link in the library note.
According to CI, the reason is no longer relevant. Leaving these as `noncomputable lemma` is harmful as it results in non-defeq instance diamonds sometimes as lean was not able to unfold the lemmas to get to the data underneath.
Since these are now `def`s, the linter requires them to have docstrings.
