Fix some dep graph links

blueprint/src/global_convex_integration.tex

@@ -97,6 +97,7 @@ \subsection{Localisation data}%
 \begin{lemma}
   \label{lem:nice_atlas}
   \lean{nice_atlas}
+  \uses{def:index_type}
   \leanok
   Let $M$ be a manifold modelled on the normed space $E$ and $(V_j)_{j ∈ J}$
   a cover of $M$ by open sets. There exists some natural number $N$ and
@@ -161,7 +162,7 @@ \subsection{Localisation data}%
 
 \begin{definition}
   \label{def:localisation_data}
-  \uses{def:convenient_indexing}
+  \uses{def:index_type}
   \lean{LocalisationData}
   \leanok
   Let $f : M → N$ be a continuous map between manifolds. A localisation data
@@ -673,7 +674,7 @@ \section{The $h$-principle for open and ample differential relations}
   \uses{lem:param_for_free, lem:ample_parameter, lem:transfer,
   lem:ex_localisation, lem:localisation_stability,
   lem:smooth_updating, lem:dist_updating, lem:inductive_htpy_construction,
-  lem:ample_iff_loc, lem:improve_htpy_loc}
+  lem:ample_iff_loc, lem:h_principle_open_ample_loc}
   Lemmas~\ref{lem:param_for_free} and~\ref{lem:ample_parameter} prove we can
   assume there are no parameters. So we start with a single formal solution $F₀$
   of $\Rel$, which is holonomic near some closed subset $A ⊂ X$. We also

blueprint/src/local_to_global.tex

@@ -35,6 +35,7 @@ \chapter{From local to global}%
 
 \begin{lemma}
   \label{lem:exists_forall_eventually_of_index_type}
+  \uses{def:index_type}
   \lean{LocallyFinite.exists_forall_eventually_of_indexType}
   \leanok
   Let $X$ be a topological space and let $Y$ be any set. Let
@@ -114,6 +115,7 @@ \chapter{From local to global}%
 $P₂^i$'' as ``$f$ can be improved in $Uᵢ$''.
 
 \begin{lemma}
+  \uses{def:index_type}
   \label{lem:inductive_construction}\uses{def:germ}\lean{inductive_construction}\leanok
   Let $X$ be a topological space and $Y$ be any set. Let $U$ be a locally
   finite family of subsets of $X$ indexed by some $\IT{N}$. Let $P₀$ be a local
@@ -204,7 +206,7 @@ \chapter{From local to global}%
   \end{itemize}
 \end{lemma}
 
-\begin{proof}\leanok\uses{lem:inductive_construction}
+\begin{proof}\leanok\uses{lem:inductive_construction, def:restrict_germ_predicate}
   Carefully checking all details is a bit technical but the strategy is as follows.
   We fix an increasing sequence $T \co \IT{N} → [0, 1)$ starting at $0$,
   say $i ↦ 1 - 1/2^i$.
@@ -309,7 +311,7 @@ \chapter{From local to global}%
 \end{lemma}
 
 \begin{proof}
-  \leanok\uses{lem:inductive_construction,lem:exists_locally_finite_subcover_of_locally}
+  \leanok\uses{lem:inductive_construction,lem:exists_locally_finite_subcover_of_locally,def:restrict_germ_predicate}
   The assumptions on the topology of $X$ and local existence of solutions
   allow to apply \Cref{lem:exists_locally_finite_subcover_of_locally} to get sequences
   of subsets $K$ and $U$ of $X$ indexed by natural numbers such that $K$ covers