## Stream: new members

### Topic: multiple names for a lemma

#### Michael Beeson (Oct 20 2020 at 07:14):

I already have lemma le_transitive. But in my paper it's Lemma 30. So I looked for it as lemma30 and did not find it.
Finally I found le_transitive. So now let's give it BOTH names so we can find it either way. OK I can do it like this:

lemma lemma30: ∀ (κ μ ℓ : M), κ ∈ 𝔽 → μ ∈ 𝔽 → ℓ ∈ 𝔽 → κ ≤ ℓ → ℓ ≤ μ → κ ≤ μ := le_transitive M


But I wish I could leave out the long formula and just write

lemma lemma30:= le_transitive M


but that is illegal for some reason.

#### Johan Commelin (Oct 20 2020 at 07:15):

Could it be

\begin{lemma} \label{le_transitive}
blabla
\end{lemma}


#### Johan Commelin (Oct 20 2020 at 07:15):

If you use a package like \usepackage{showkeys} then you will even see the latex labels in the margin of your PDF

#### Johan Commelin (Oct 20 2020 at 07:16):

Because if you insert a lemma before "Lemma 30", you'll have a lot of renaming to do, if you do it your way. So I would suggest trying to write that 30 in as few places as possible. Preferably nowhere at all.

#### Mario Carneiro (Oct 20 2020 at 07:17):

you can use alias for this

#### Mario Carneiro (Oct 20 2020 at 07:17):

or def foo := @bar

#### Mario Carneiro (Oct 20 2020 at 07:17):

even if bar is a theorem

#### Mario Carneiro (Oct 20 2020 at 07:18):

although the linter will yell at you

#### Michael Beeson (Oct 20 2020 at 07:18):

Aha! That would be VERY useful. The only reason I'm naming these lemmas with numbers in Lean is so I can work with the pdf on one monitor and the Lean file on the other monitor. Since sync is more or less dysfunctional in TeXShop I need to work with the pdf mostly. I've already had to insert a lemma a couple of times. It's obviously a wrong way to work,
but I'm almost done now with this paper.

#### Mario Carneiro (Oct 20 2020 at 07:19):

If you are writing a formalization paper, you should definitely put the lemma names in the paper like Johan says

#### Mario Carneiro (Oct 20 2020 at 07:19):

don't do it the other way around, putting those terrible latex names in the formalization

#### Johan Commelin (Oct 20 2020 at 07:20):

@Michael Beeson Even in your setup, where you want to look at the PDF, instead of the tex source, I think you should use {showkeys}

#### Mario Carneiro (Oct 20 2020 at 07:20):

well, Johan's using them as labels but I would put them also in the print, i.e. \begin{lemma}[(\texttt{le_transitive})] ...

#### Johan Commelin (Oct 20 2020 at 07:24):

Why not let a package do that for you?

#### Mario Carneiro (Oct 20 2020 at 07:24):

I have nothing against it, I've never used showkeys

#### Mario Carneiro (Oct 20 2020 at 07:25):

not sure about using the margin for this though, that's often off limits depending on the stylesheet / target venue

#### Johan Commelin (Oct 20 2020 at 07:27):

At least one of those packages that shows labels in print is pretty configurable. I always forget which one is which.

#### Mario Carneiro (Oct 20 2020 at 07:28):

also I don't know whether I would want this for all \labels in the file, since I use \label also for section references and those don't get a texttt gloss

#### Johan Commelin (Oct 20 2020 at 07:32):

Well, I love it that they also show up in the margin while I'm writing the text. For the final product, I agree that it would be good to have a more polished solution.

Last updated: May 11 2021 at 00:31 UTC