With humility I will say that I don't like this solution.
In mathematics functions have domains and codomains. Two functions are equal if their domains are equal, their codomains are equal, and for all the values in the domain they return the same values in the codomain.
A mathematician who doesn't know anything about type theory, but hears Lean is good at formalizing math, will expect the division function to have the domain R x (R\{0}). Modifying the domain to be R x R and returning a garbage value for the added points is not a good solution. Maybe it works "in real life", but you always need to carry with you an invisible asterisk and footnote that Lean did the right thing only assuming you asked the right question.
Again, being humble (my Lean experience is about one hour in total, spread across several sessions), I think it would be better to invest a bit more time upfront and always define properly the domain of the function used, rather than introduce edge cases that can bite you in the back twenty five theorems down the road.
In mathematics functions have domains and codomains. Two functions are equal if their domains are equal, their codomains are equal, and for all the values in the domain they return the same values in the codomain.
A mathematician who doesn't know anything about type theory, but hears Lean is good at formalizing math, will expect the division function to have the domain R x (R\{0}). Modifying the domain to be R x R and returning a garbage value for the added points is not a good solution. Maybe it works "in real life", but you always need to carry with you an invisible asterisk and footnote that Lean did the right thing only assuming you asked the right question.
Again, being humble (my Lean experience is about one hour in total, spread across several sessions), I think it would be better to invest a bit more time upfront and always define properly the domain of the function used, rather than introduce edge cases that can bite you in the back twenty five theorems down the road.