Solution to the Challenge

The declaration of Challenge.lean, proved. It is a thin bridge to NashEmbedding.nashCompact; the only difference is bookkeeping: the library states the pullback condition through the predicate PullsBackEuclidean, whose definition unfolds to exactly the Challenge's clause (toEuclid is the identity map exposing a tangent vector to Euclidean space as a point of it).

The underlying NashEmbedding development was substantially formalized by Aristotle (Harmonic); see the repository provenance record.

theorem NashEmbeddingTheorem.nash_isometric_embedding {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] (g : Bundle.ContMDiffRiemannianMetric I (↑⊤) E (TangentSpace I)) : ∃ (q : ℕ) (w : M → EuclideanSpace ℝ (Fin q)), ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin q))) (↑⊤) w ∧ Function.Injective w ∧ ∀ (x : M) (v v' : TangentSpace I x), ((g.inner x) v) v' = inner ℝ ((mfderiv% w x) v) ((mfderiv% w x) v')

Nash's isometric embedding theorem, proved in NashEmbedding.nashCompact. Axioms: propext, Classical.choice, Quot.sound.