Merge branch 'PartialHomeomorph1' of github.com:scholzhannah/mathlib4 into PartialHomeomorph1

Author: scholzhannah

Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

@@ -44,7 +44,6 @@ protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z wher
   open_target := e'.open_target
   continuousOn_toFun := e'.continuousOn.comp e.continuousOn <| h ▸ e.mapsTo
   continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.mapsTo_symm
-  continuousOn_invFun := e.continuousOn_symm.comp e'.continuousOn_symm <| h.symm ▸ e'.mapsTo_symm
 
 /-- Composing two open partial homeomorphisms, by restricting to the maximal domain where their
 composition is well defined.