This sort of convenient semi-arbitrary extension of a partial function is ubiquitous in Lean 4 mathlib, the most active mathematics formalization project today. It turns out that the most convenient way to do informal math and formal math differ in this aspect.