remoted attempt to have two lean tags on one proposition

emilyriehl · Oct 8, 2024 · 010628d · 010628d
1 parent 4a9559b
commit 010628d
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
@@ -892,7 +892,7 @@ \section{Change of base}\label{sec:change-of-base}
 \begin{corollary}\label{cor:free-underlying-2-adj}
   \uses{prop:change-of-base-adjunction}
   \lean{CategoryTheory.categoryForgetEnrichment}
-  \lean{CategoryTheory.EnrichedFunctor.forget}
+%  \lean{CategoryTheory.EnrichedFunctor.forget}
   \leanok For any cartesian closed category $\cV$ with coproducts, the underlying category construction and free category construction define  adjoint 2-functors
 \begin{center}
 \begin{tikzcd}[column sep=large]

diff --git a/blueprint/src/print.pdf b/blueprint/src/print.pdf