mathlib

b4d2ce45 - chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/function): review (#6306)

chore(data/equiv/local_equiv,topology/local_homeomorph,data/set/function): review (#6306) ## `data/equiv/local_equiv`: * move `local_equiv.inj_on` lemmas closer to each other, add missing lemmas; * rename `local_equiv.bij_on_source` to `local_equiv.bij_on`; * rename `local_equiv.inv_image_target_eq_souce` to `local_equiv.symm_image_target_eq_souce`; ## `data/set/function` * add `set.inj_on.mem_of_mem_image`, `set.inj_on.mem_image_iff`, `set.inj_on.preimage_image_inter`; * add `set.left_inv_on.image_image'` and `set.left_inv_on.image_image`; * add `function.left_inverse.right_inv_on_range`; * move `set.inj_on.inv_fun_on_image` to golf the proof; ## `topology/local_homeomorph` * add lemmas like `local_homeomorph.inj_on`; * golf the definition of `open_embedding.to_local_homeomorph`, make `f` explicit.