local homeomorph

Stream: mathlib4

[Yury G. Kudryashov]

I've started porting Topology.LocalHomeomorph. Since LocalEquiv is not a FunLike, the coercion to function is going to unfold to e.toLocalEquiv.toFun. This means that docs#local_homeomorph.symm_to_local_equiv will unfold e.symm.toFun to e.toLocalEquiv.symm.toFun which is the opposite of docs#local_homeomorph.coe_coe_symm (which becomes a syntatic rfl).

[Yury G. Kudryashov]

What should I do?

1. Proceed with (e : α → β) = e.toLocalEquiv.toFun, adjust some simp lemmas, await for broken proofs down the import chain.
2. Define LocalHomeomorph.toFun', use it as coercion, leave the refactor till after the porting.

[Yury G. Kudryashov]

3. Something I missed.

[Yury G. Kudryashov]

Let me tag some users of local_homeomorph: @Heather Macbeth @Sebastien Gouezel @Floris van Doorn @Nicolò Cavalleri @Scott Morrison @Eric Wieser @Patrick Massot

[Floris van Doorn]

Ah, you cannot make then FunLike instances because the toFun map is not injective...

Going with option 2 might be best for now, since it's the behavior that is most similar to Lean 3.