From 29c536b3a72e63299206d09f9bad0b9adb5ac622 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgang@math.uni-bonn.de>
Date: Fri, 17 Jan 2025 23:32:27 +0100
Subject: [PATCH] fix(blueprint): declaration name, for the mathlib bump

---
 blueprint/src/global_convex_integration.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/blueprint/src/global_convex_integration.tex b/blueprint/src/global_convex_integration.tex
index a0874729..90178104 100644
--- a/blueprint/src/global_convex_integration.tex
+++ b/blueprint/src/global_convex_integration.tex
@@ -330,7 +330,7 @@ \subsection{Jets spaces}
 
 \begin{lemma}
 \label{lem:one_jet_extension_prop}
-\lean{Smooth.oneJetExt}
+\lean{ContMDiff.oneJetExt}
 \leanok
 \uses{def:one_jet_extension}
 For every smooth map $f \co M → N$,