multiple names for a lemma

Stream: new members

[Michael Beeson]

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]

Could it be

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

in your paper?

[Johan Commelin]

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

[Johan Commelin]

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]

you can use alias for this

[Mario Carneiro]

or def foo := @bar

[Mario Carneiro]

even if bar is a theorem

[Mario Carneiro]

although the linter will yell at you

[Michael Beeson]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

@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]

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]

Why not let a package do that for you?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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.