The strict transforms on cons

The recursion of the strict transforms H_0 = H, H_{i+1} = closure of π_i⁻¹(H_i ∖ Z_i) along a sequence (strictTransformSeq, the "birational transform H⁰_i of H⁰" of [Kol07, Definition 78]) restarts, on the constructor form cons ψ hY rest, from the strict transform of H by the first blow-down, with centre Y: an induction on the stage (cons_strictTransformSeqAux_succ, rfl at every step because cons puts the head before the fields of rest by Fin.cases over finStages), with Z_0 = cosupp I_Y = Y.

theorem AnalyticManifold.FiniteSuccession.cons_strictTransformSeqAux_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (H : Set M.carrier) (k : ℕ) (h : k + 1 < (cons ψ hY rest).length + 1) : (cons ψ hY rest).strictTransformSeqAux H (k + 1) h = rest.strictTransformSeqAux (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ hY)) hY.idealSheaf.support H) k ⋯

The strict transforms of H along cons ψ hY rest after the first step are those of rest starting from the strict transform of H by the first blow-down, with centre cosupp I_Y.

theorem AnalyticManifold.FiniteSuccession.cons_strictTransformSeq_succ {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (H : Set M.carrier) (hY : Manifold.IsClosedSubmanifold ψ Y c) (rest : (Manifold.blowUp ψ hY).FiniteSuccession) (j : Fin (rest.length + 1)) : (cons ψ hY rest).strictTransformSeq H j.succ = rest.strictTransformSeq (Manifold.strictTransformSet (⇑(Manifold.blowUpπ ψ hY)) Y H) j

The recursion of the strict transforms on the constructor form, indexed by Fin and with Z_0 = Y.