# extern lemma declaration

Is it possible to something like this:

\begin{theorm}
foo equal bar
\end{theorem}
\begin{proof}
\extern{lemma-fu}
With this, we will do … % A lot of text
\end{proof}

\begin{lemma}
\label{lemma-fu}
some statement
\end{lemma}
\begin{proof}
proof-of-lemma
\end{proof}


I want imagine command \extern to insert lemma into proof of theorem. With verbdef I can do reverse -- write formulation of lemma in proof of theorem and refer to it later, but It is less readable in source code.

-
What precisely do you want \extern{lemma-fu} to do? Insert the number corresponding to lemma-fu or the whole statement? – egreg Jan 1 '13 at 17:48
I want it to insert everything(exept label command} between \begin{lemma} and \end{lemma}. In my example I want it to insert some statement. – KAction Jan 1 '13 at 18:30
Do you really think it's a good idea? I don't. – egreg Jan 1 '13 at 18:32
Well, let me explain why I want it. When I read some proof I hate to read references to lemma 1.4.5, that makes me to scroll to it and back. So I want declarations of lemmas to be put into proof, and lemmas to be proved later in text. Why? Because I want overview first, and details later. I already said, that I can put full lemmas into proof and refer to it later (via verbdef), but mind the source code. – KAction Jan 1 '13 at 18:43
If you lemmas appear always before \extern and have only non-fragile content, one could define something using the with environ package. Would that help? Otherwise, one would need to use external files and/or several TeX runs. – Marcus Bitzl Feb 12 '14 at 17:04

Here's a quick solution which saves the lemma to a file. Note that it doesn't have any warnings if a lemma can't be found. It requires two TeX runs:

\documentclass[12pt]{minimal}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\usepackage{amsthm}

\usepackage{environ,etoolbox}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}

\makeatletter
\NewEnviron{Lemma}[1]{
\protected@write\@mainaux{}{
\csgdef{\detokenize{Lemma@#1}}{\BODY}
}
\begin{lemma}\label{#1}
\BODY
\end{lemma}
}

\newcommand{\extern}[1]{\textbf{Lemma \ref{#1}:} \@nameuse{\detokenize{Lemma@#1}}}
\makeatother

\begin{document}
\begin{theorem}
foo equal bar
\end{theorem}
\begin{proof}
\extern{lemma:fu}
With this, we will do … % A lot of text
\end{proof}

\begin{Lemma}{lemma:fu}
A cool lemma.
\end{Lemma}
\begin{proof}
That is true!
\end{proof}
\end{document}

-