@[reducible, inline]

abbrev GaussMap.unitSphere (n : ℕ) : Set (EuclideanSpace ℝ (Fin (n + 1)))

theorem GaussMap.smooth_local_diffeo_compact_to_sphere_bijective {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin (n + 1)))) (hM_hyp : Hypersurface.IsHypersurface M) (hM_compact : IsCompact M) (hM_connected : IsConnected M) (hn : 2 ≤ n) (φ : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))) (hφ_maps : ∀ y ∈ M, φ y ∈ unitSphere n) (hφ_smooth : ContDiffOn ℝ ⊤ φ M) (hφ_tangent_iso : ∀ y ∈ M, ∀ (ψ : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), Hypersurface.IsLocalDefiningFunction ψ M y → ∀ v ∈ Hypersurface.tangentSpace ψ y, (fderiv ℝ φ y) v = 0 → v = 0) : Function.Bijective fun (y : ↑M) => ⟨φ ↑y, ⋯⟩