The chart-defined $C^1$ topology equals the tangent-map $C^1$ topology on $\mathrm{Diff}^1(M)$

Let $M$ be a compact Hausdorff smooth manifold of dimension $n$ without boundary, and let $\mathrm{Diff}^1(M)$ be the set of its $C^1$ diffeomorphisms. Two topologies on $\mathrm{Diff}^1(M)$ are in use:

1. the chart $C^1$ topology $\tau_{\mathrm{chart}}$, generated by the basic neighbourhoods $\mathcal N^1(f;\varphi,\psi,K,\varepsilon)$ that control $g$ and its first derivative in charts on compact sets (definition ClosingLemma_DiffeoCrTopology with $r=1$);
2. the tangent-map $C^1$ topology $\tau_{T}$, the coarsest topology making $g\mapsto Tg$ continuous, where $Tg\colon TM\to TM$ is the tangent map and $C(TM,TM)$ carries the compact-open topology (published definition BCWCentralizer_Basic).

The theorem states that they coincide:

With this identification, Pugh's $C^1$ closing lemma, as published on the platform for $\tau_T$, is exactly the case $r=1$ of the mission's goal.

Formalization Note Both topologies live on the same Lean type M ≃ₘ^1⟮𝓡 n, 𝓡 n⟯ M; the statement is an equality of TopologicalSpace structures.