The Mathlib-only effective Cartier ideal sheaves and blow-ups are the library's

Scheme.IdealSheafData.IsEffectiveCartier and Scheme.Hom.IsBlowUpAlong (Hironaka.Scheme.BlowUp.BlowUpAlong.Defs), defined from Mathlib's notions alone, are the library's Scheme.IdealSheafData.IsInvertible and IsBlowUp: Scheme.IdealSheafData.isEffectiveCartier_iff_isInvertible and Scheme.Hom.isBlowUpAlong_iff_isBlowUp.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isEffectiveCartier_iff_isInvertible {X : Scheme} (J : X.IdealSheafData) : J.IsEffectiveCartier ↔ J.IsInvertible

An effective Cartier ideal sheaf is an invertible one, in the library's sense.

theorem AlgebraicGeometry.Scheme.Hom.isBlowUpAlong_iff_isBlowUp {X B : Scheme} (π : B ⟶ X) (I : X.IdealSheafData) : IsBlowUpAlong π I ↔ IsBlowUp I π

π.IsBlowUpAlong I is the library's IsBlowUp I π.