fix some errors + push for cache

Author: scholzhannah

Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

@@ -43,7 +43,7 @@ protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z wher
   open_source := e.open_source
   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'.symm_mapsTo
+  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.

Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

@@ -201,7 +201,7 @@ def disjointUnion (e e' : OpenPartialHomeomorph X Y) [∀ x, Decidable (x ∈ e.
         (by rw [e.open_source.inter_frontier_eq, (Hs.symm.frontier_right e'.open_source).inter_eq])
         (by
           rw [e.open_source.inter_frontier_eq]
-          exact eqOn_empty _ _)).replaceEquiv
+          exact eqOn_empty _ _)).replacePartialEquiv
     (e.toPartialEquiv.disjointUnion e'.toPartialEquiv Hs Ht)
     (PartialEquiv.disjointUnion_eq_piecewise _ _ _ _).symm
 

Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

@@ -98,6 +98,7 @@ protected theorem continuousOn : ContinuousOn e e.source :=
 theorem continuousOn_symm : ContinuousOn e.symm e.target :=
   e.continuousOn_invFun
 
+@[simp, mfld_simps]
 theorem mk_coe (e : PartialEquiv X Y) (h1 h2 h3 h4) :
     (OpenPartialHomeomorph.mk e h1 h2 h3 h4 : X → Y) = e :=
   rfl