The local Hadamard lemma for a single coordinate on an unbundled manifold

The local Hadamard lemma vanishingStalk_zeroSet_eq_span_coord (Hironaka/Resolution/Analytic/Wlo09/BoundaryBridge.lean) reads the vanishing stalk of the zero set φ.source ∩ {z_σ = 0} of chart coordinates at a point of the chart as the span of those coordinates, for a bundled manifold M : AnalyticManifold (its proof restricts to the chart's source, M.restrict U). A statement that binds its manifold as a charted type, with the manifold structure as instances, may need the vanishing stalk of a strict transform at a point of a blow-up chart, where the strict transform is the zero set of one coordinate on the chart's source (strictTransform_inter_source_of_ne, strictTransform_inter_source_of_ne_off) but is not known to be a closed submanifold without a simple-normal-crossing hypothesis on the centre. vanishingStalk_eq_span_coord_of_forall_mem_iff is the single-coordinate form of the local lemma for such a manifold, with no hypothesis on Z beyond its description on the chart's source: the bundled lemma applied to the bundle ⟨M⟩ of the charted type (whose instance fields are exactly the binders), plus the unit-ideal case off Z. Not in the sources; the coordinate description of the members of a simple normal crossing divisor is [Kol07, Definition 24].

theorem Hironaka.Manifold.vanishingStalk_eq_span_coord_of_forall_mem_iff {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [T2Space M] [SecondCountableTopology M] {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {Z : Set M} {k : Fin n} (hS : ∀ x ∈ φ.source, x ∈ Z ↔ ψ (↑φ x) k = 0) {p : M} (hp : p ∈ φ.source) : Manifold.vanishingStalk Z p = Ideal.span {Manifold.coord E ψ φ hφ hp k}

The vanishing stalk at a point p of a chart φ of a set Z that is, on the chart's source, the zero set of the coordinate k, is spanned by that coordinate, with no closedness or submanifold hypothesis on Z. The single-coordinate form of vanishingStalk_zeroSet_eq_span_coord for an unbundled manifold: the vanishing stalk sees only Z ∩ φ.source (vanishingStalk_inter_of_mem_nhds); on Z the bundled lemma at ⟨M⟩ : AnalyticManifold 𝕜 E (whose five instance fields are exactly the binders here) gives the span of the single coordinate (singleEmb); off Z, p lies outside the closure of Z ∩ φ.source (the open φ.source ∩ {ψ (φ ·) k ≠ 0} contains p and misses it), so both sides are the unit ideal (vanishingStalk_eq_top_of_notMem_closure, isUnit_coord_of_ne_zero). Not in the sources.