The simple locus of a reduced complex space is dense

Over ℂ, the simple points of a reduced complex analytic space are dense (dense_reg_of_isReduced_complex: [Fre17, II 5.13], proved in Hironaka/Space/RegDensity from Noether normalization by a primitive element and the graph description of Rückert's parametrization); read in the ambient manifold, |J| ⊆ closure (regSet J) for J with radical stalks (cosupport_subset_closure_regSet). This is the density Kollár's proof of Corollary 22 uses ([Kol07, Corollary 22, proof]; compare the remark after Main Theorem I in [Hir64, Ch. 0, §3]).

theorem Manifold.dense_reg_of_isReduced_complex (X : AnalyticSpace ℂ) (hX : X.IsReduced) : Dense X.regularLocus

The simple points of a reduced complex analytic space are dense [Fre17, II 5.13]: the general theorem of Hironaka/Space/RegDensity, at the hypotheses proved for ℂ (Noether normalization by a primitive element and the graph description of Rückert's parametrization).

theorem Manifold.cosupport_subset_closure_regSet {n : ℕ} {A : AnalyticManifold ℂ (Fin n → ℂ)} (J : A.IdealSheaf) (hJ : ∀ (x : ↑↧A.carrier), (IdealSheaf.stalkIdeal J x).IsRadical) : IdealSheaf.support J ⊆ closure J.regSet

Over ℂ, for J with radical stalks, the simple locus of V(J) read in the ambient is dense in the support |J|.