Proof of Proposition 3, p. 50 — substituting (32) into (29) gives (31)

Let $\sigma>0$, $s\in(0,1)$ and $\delta\in\mathbb R$ with $\sigma^2<s\delta$ (the shorting region $s>s^*$). Let $\Phi=\Phi(\sigma,\delta,s)$ be the closed-form shorting cost (31) and $\Gamma=\Gamma(\sigma,\delta,s)$ the closed-form lending yield (32). Then the shorting-cost equation (29) holds on the region:

With the previous milestone, this shows that $(\Phi,\Gamma)$ given by (31)–(32) solves the whole system (29)–(30) on the shorting region.

Formalization Note On the region both indicators equal one; the Lean uses the definitions costOne and yieldOne of (31) and (32), whose common guard $\sigma^2<s\delta$ is the hypothesis.