Affine section cover of a blow-up of an affine scheme

Let $X$ be an affine scheme, $I$ an ideal sheaf on $X$, and $\pi:B\to X$ a blow-up of $I$. If the line bundle $J$ with $\iota:J\to\mathcal O_B$ presents the pullback of $I$, then there is a family of sections of $J$ whose iso-opens cover $B$ and are all affine.

Notation. The iso-open of $s$ (SectionOpens.isoOpen s) is the union of the opens on which the morphism $s$ restricts to an isomorphism. PresentsPullbackIdeal I f J ι says that $\iota:J\to\mathcal O_Y$ is a monomorphism whose image on affine opens is the extension of $I$ along $f$. IsBlowup I π says that $I$ pulls back to an invertible ideal along $\pi$ and that $\pi$ is universal with this property.

Formalization Note The statement is verbatim from OpenAI's Lean development, with Definitions files of this development imported in place of the upstream modules; these are supporting code for the statement.