Inversion is discontinuous

Stream: mathlib4

[Theo Sandstrom]

I am a new lean user, interested in contributing to the Mathlib codebase. I saw that #5939 is marked as a good first issue. Can somebody point me towards where in the library I should look to familiarize myself with the relevant definitions, and where such a lemma would belong?

[Kalle Kytölä]

As a first guess, the lemma might seem to belong to Mathlib/Geometry/Euclidean/Inversion/Calculus.lean like the content in the PR #5937 mentioned in the issue. But while working on the lemma, it may be a good idea to temporarily create a new file, so as to keep all of Mathlib's cache untouched. (By contrast if you edit an already existing file, anything depending on it would have to be built again.) The location can then be fixed once the proof is ready. And in a temporary file also you can temporarily import Mathlib (to be sure to have everything relevant available) and only #minimize_imports once you are done.

As for how to familiarize yourself with the relevant definitions, I would start from somewhere (like the file above or the file Mathlib.Geometry.Euclidean.Inversion.Basic it imports) and read the "module docstring" at the top of the file. One can also "hover" over relevant-looking or interesting-looking terms to see their types and docstrings, and potentially "right-click + Go to definition" to get more details and context. But the question is very open-ended and depends a lot on what you know and are familiar with already... I recommend just playing around and asking if something specific looks puzzling.