Commit 2024-01-27 11:43 ca91ff1e

refactor(PartialHomeomorph): make [Nonempty s] explicit (#9894) Subsets aren't going to have Nonempty instances on them, typically, so one would have to manually construct a term of [Nonempty s] whenever PartialHomeomorph.subtypeRestr is used. Turning this instance argument explicit, (hs : Nonempty s) would help us avoid @PartialHomeomorph.subtypeRestr _ _ _ _ constructions or haveI : Nonempty .... Its only downstream effect currently is in ChartedSpace.lean.