The same widget Lean Studio shows in its Infoview, fed the numbers Lean computes. Proofs and source: github.com/keithadler/penrose-lean. MIT License.