changes from review + push for cache

Author: scholzhannah

Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

@@ -122,7 +122,7 @@ theorem isOpen_image_iff_of_subset_source {s : Set X} (hs : s ⊆ e.source) :
 
 /-- A `PartialEquiv` with continuous open forward map and open source is a
 `OpenPartialHomeomorph`. -/
-@[simps toPartialHomeomorph_toPartialEquiv]
+@[simps toPartialHomeomorph]
 def ofContinuousOpenRestrict (e : PartialEquiv X Y) (hc : ContinuousOn e e.source)
     (ho : IsOpenMap (e.source.restrict e)) (hs : IsOpen e.source) : OpenPartialHomeomorph X Y where
   toPartialEquiv := e
@@ -145,7 +145,7 @@ theorem coe_ofContinuousOpenRestrict_symm (e : PartialEquiv X Y) (hc : Continuou
 
 /-- A `PartialEquiv` with continuous open forward map and open source is a
 `OpenPartialHomeomorph`. -/
-@[simps! toPartialHomeomorph_toPartialEquiv]
+@[simps! toPartialHomeomorph]
 def ofContinuousOpen (e : PartialEquiv X Y) (hc : ContinuousOn e e.source) (ho : IsOpenMap e)
     (hs : IsOpen e.source) : OpenPartialHomeomorph X Y :=
   ofContinuousOpenRestrict e hc (ho.restrict hs) hs

Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

@@ -37,7 +37,7 @@ variable (e' : OpenPartialHomeomorph Y Z)
 
 /-- Composition of two open partial homeomorphisms when the target of the first and the source of
 the second coincide. -/
-@[simps! apply symm_apply toPartialHomeomorph_toPartialEquiv, simps! -isSimp source target]
+@[simps! apply symm_apply toPartialHomeomorph, simps! -isSimp source target]
 protected def trans' (h : e.target = e'.source) : OpenPartialHomeomorph X Z where
   toPartialEquiv := PartialEquiv.trans' e.toPartialEquiv e'.toPartialEquiv h
   open_source := e.open_source
@@ -99,7 +99,7 @@ theorem inv_image_trans_target : e'.symm '' (e.trans e').target = e'.source ∩
 
 theorem trans_assoc (e'' : OpenPartialHomeomorph Z Z') :
     (e.trans e').trans e'' = e.trans (e'.trans e'') :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective <| e.1.trans_assoc _ _
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| e.1.trans_assoc _ _
 
 @[simp, mfld_simps]
 theorem trans_refl : e.trans (OpenPartialHomeomorph.refl Y) = e :=
@@ -131,7 +131,7 @@ theorem ofSet_trans_ofSet {s : Set X} (hs : IsOpen s) {s' : Set X} (hs' : IsOpen
   ext <;> simp [hs'.interior_eq]
 
 theorem restr_trans (s : Set X) : (e.restr s).trans e' = (e.trans e').restr s :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective <|
+  toPartialEquiv_comp_toPartialHomeomorph_injective <|
     PartialEquiv.restr_trans e.toPartialEquiv e'.toPartialEquiv (interior s)
 
 end trans
@@ -213,7 +213,7 @@ def transOpenPartialHomeomorph (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z)
 
 theorem transOpenPartialHomeomorph_eq_trans (e : X ≃ₜ Y) (f' : OpenPartialHomeomorph Y Z) :
     e.transOpenPartialHomeomorph f' = e.toOpenPartialHomeomorph.trans f' :=
-  OpenPartialHomeomorph.toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective
+  OpenPartialHomeomorph.toPartialEquiv_comp_toPartialHomeomorph_injective
     <| Equiv.transPartialEquiv_eq_trans _ _
 
 @[simp, mfld_simps]

Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

@@ -76,7 +76,7 @@ section Prod
 
 /-- The product of two open partial homeomorphisms, as an open partial homeomorphism on the product
 space. -/
-@[simps! (attr := mfld_simps) -fullyApplied toPartialHomeomorph_toPartialEquiv apply,
+@[simps! (attr := mfld_simps) -fullyApplied toPartialHomeomorph apply,
   simps! -isSimp source target symm_apply]
 def prod (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y') :
     OpenPartialHomeomorph (X × Y) (X' × Y') where
@@ -100,7 +100,7 @@ theorem refl_prod_refl : (OpenPartialHomeomorph.refl X).prod (OpenPartialHomeomo
 theorem prod_trans (e : OpenPartialHomeomorph X Y) (f : OpenPartialHomeomorph Y Z)
     (e' : OpenPartialHomeomorph X' Y') (f' : OpenPartialHomeomorph Y' Z') :
     (e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f') :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective <| e.1.prod_trans ..
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| e.1.prod_trans ..
 
 theorem prod_eq_prod_of_nonempty {eX eX' : OpenPartialHomeomorph X X'}
     {eY eY' : OpenPartialHomeomorph Y Y'} (h : (eX.prod eY).source.Nonempty) :
@@ -137,7 +137,7 @@ variable {ι : Type*} [Finite ι] {X Y : ι → Type*} [∀ i, TopologicalSpace
   [∀ i, TopologicalSpace (Y i)] (ei : ∀ i, OpenPartialHomeomorph (X i) (Y i))
 
 /-- The product of a finite family of `OpenPartialHomeomorph`s. -/
-@[simps! toPartialHomeomorph_toPartialEquiv apply symm_apply source target]
+@[simps! toPartialHomeomorph apply symm_apply source target]
 def pi : OpenPartialHomeomorph (∀ i, X i) (∀ i, Y i) where
   toPartialEquiv := PartialEquiv.pi fun i => (ei i).toPartialEquiv
   open_source := isOpen_set_pi finite_univ fun i _ => (ei i).open_source
@@ -164,7 +164,7 @@ To ensure the maps `toFun` and `invFun` are inverse of each other on the new `so
 the definition assumes that the sets `s` and `t` are related both by `e.is_image` and `e'.is_image`.
 To ensure that the new maps are continuous on `source`/`target`, it also assumes that `e.source` and
 `e'.source` meet `frontier s` on the same set and `e x = e' x` on this intersection. -/
-@[simps! -fullyApplied toPartialHomeomorph_toPartialEquiv apply]
+@[simps! -fullyApplied toPartialHomeomorph apply]
 def piecewise (e e' : OpenPartialHomeomorph X Y) (s : Set X) (t : Set Y) [∀ x, Decidable (x ∈ s)]
     [∀ y, Decidable (y ∈ t)] (H : e.IsImage s t) (H' : e'.IsImage s t)
     (Hs : e.source ∩ frontier s = e'.source ∩ frontier s)
@@ -226,8 +226,7 @@ def transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) : OpenPart
 
 theorem transHomeomorph_eq_trans (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z) :
     e.transHomeomorph f' = e.trans f'.toOpenPartialHomeomorph :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective
-    <| PartialEquiv.transEquiv_eq_trans _ _
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.transEquiv_eq_trans _ _
 
 @[simp, mfld_simps]
 theorem transHomeomorph_transHomeomorph (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z)

Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

@@ -62,8 +62,7 @@ variable (e : OpenPartialHomeomorph X Y)
 /-! Basic properties; inverse (symm instance) -/
 section Basic
 /-- Coercion of an open partial homeomorphisms to a function. We don't use `e.toFun` because it is
-actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.
-While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs. -/
+actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`. -/
 @[coe] def toFun' : X → Y := e.toFun
 
 /-- Coercion of an `OpenPartialHomeomorph` to function.
@@ -87,15 +86,17 @@ def Simps.symm_apply (e : OpenPartialHomeomorph X Y) : Y → X := e.symm
 
 initialize_simps_projections OpenPartialHomeomorph (toFun → apply, invFun → symm_apply)
 
+@[fun_prop]
 protected theorem continuousOn : ContinuousOn e e.source :=
   e.continuousOn_toFun
 
+@[fun_prop]
 theorem continuousOn_symm : ContinuousOn e.symm e.target :=
   e.continuousOn_invFun
 
 @[simp, mfld_simps]
-theorem mk_coe (e : PartialEquiv X Y) (a b c d) :
-    (OpenPartialHomeomorph.mk (.mk e a b) c d : X → Y) = e :=
+theorem mk_coe (e : PartialEquiv X Y) (h1 h2 h3 h4) :
+    (OpenPartialHomeomorph.mk (.mk e h1 h2) h3 h4 : X → Y) = e :=
   rfl
 
 @[simp, mfld_simps]
@@ -107,6 +108,11 @@ theorem toPartialHomeomorph_injective :
     Injective (toPartialHomeomorph : OpenPartialHomeomorph X Y → PartialHomeomorph X Y)
   | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl
 
+theorem toPartialEquiv_comp_toPartialHomeomorph_injective :
+    Injective (PartialHomeomorph.toPartialEquiv ∘ toPartialHomeomorph :
+      OpenPartialHomeomorph X Y → PartialEquiv X Y) :=
+  PartialHomeomorph.toPartialEquiv_injective.comp toPartialHomeomorph_injective
+
 /- Register a few simp lemmas to make sure that `simp` puts the application of a local
 homeomorphism in its normal form, i.e., in terms of its coercion to a function. -/
 @[simp, mfld_simps]
@@ -141,7 +147,7 @@ theorem coe_toPartialHomeomorph : (e.toPartialHomeomorph : X → Y) = e :=
 theorem coe_toPartialHomeomorph_symm : (e.toPartialHomeomorph.symm : Y → X) = e.symm :=
   rfl
 
-/-- Variant of `map_source`, stated for images of subsets of `source`. -/
+/-- Variant of `map_source`, stated in terms of subsets. -/
 lemma map_source'' : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
 
@@ -166,6 +172,8 @@ protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 protected theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
   e.symm.mapsTo
 
+@[deprecated (since := "2026-05-18")] alias symm_mapsTo := OpenPartialHomeomorph.mapsTo_symm
+
 protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv
 
 protected theorem rightInvOn : RightInvOn e.symm e e.target := fun _ => e.right_inv

Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean

@@ -171,7 +171,7 @@ theorem isOpen_iff (h : e.IsImage s t) : IsOpen (e.source ∩ s) ↔ IsOpen (e.t
     h.preimage_eq' ▸ e.isOpen_inter_preimage hs⟩
 
 /-- Restrict an `OpenPartialHomeomorph` to a pair of corresponding open sets. -/
-@[simps! -fullyApplied apply symm_apply toPartialHomeomorph_toPartialEquiv]
+@[simps! -fullyApplied apply symm_apply toPartialHomeomorph]
 def restr (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)) : OpenPartialHomeomorph X Y where
   toPartialEquiv := h.toPartialEquiv.restr
   open_source := hs
@@ -254,8 +254,8 @@ theorem restr_toPartialEquiv' (s : Set X) (hs : IsOpen s) :
 
 theorem restr_eq_of_source_subset {e : OpenPartialHomeomorph X Y} {s : Set X} (h : e.source ⊆ s) :
     e.restr s = e :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective
-    <| PartialEquiv.restr_eq_of_source_subset <| interior_maximal h e.open_source
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.restr_eq_of_source_subset <|
+    interior_maximal h e.open_source
 
 @[simp, mfld_simps]
 theorem restr_univ {e : OpenPartialHomeomorph X Y} : e.restr univ = e :=
@@ -360,8 +360,7 @@ theorem Set.EqOn.restr_eqOn_source {e e' : OpenPartialHomeomorph X Y}
 
 theorem eq_of_eqOnSource_univ {e e' : OpenPartialHomeomorph X Y} (h : e ≈ e') (s : e.source = univ)
     (t : e.target = univ) : e = e' :=
-  toPartialHomeomorph_injective <| PartialHomeomorph.toPartialEquiv_injective <|
-    PartialEquiv.eq_of_eqOnSource_univ _ _ h s t
+  toPartialEquiv_comp_toPartialHomeomorph_injective <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t
 
 variable {s : Set X}
 

Mathlib/Topology/PartialHomeomorph/Defs.lean

@@ -62,8 +62,7 @@ variable (e : PartialHomeomorph X Y)
 /-! Basic properties; inverse (symm instance) -/
 section Basic
 /-- Coercion of a partial homeomorphisms to a function. We don't use `e.toFun` because it is
-actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`.
-While we may want to switch to this behavior later, doing it mid-port will break a lot of proofs. -/
+actually `e.toPartialEquiv.toFun`, so `simp` will apply lemmas about `toPartialEquiv`. -/
 @[coe] def toFun' : X → Y := e.toFun
 
 /-- Coercion of a `PartialHomeomorph` to function.
@@ -87,14 +86,16 @@ def Simps.symm_apply (e : PartialHomeomorph X Y) : Y → X := e.symm
 
 initialize_simps_projections PartialHomeomorph (toFun → apply, invFun → symm_apply)
 
+@[fun_prop]
 protected theorem continuousOn : ContinuousOn e e.source :=
   e.continuousOn_toFun
 
+@[fun_prop]
 theorem continuousOn_symm : ContinuousOn e.symm e.target :=
   e.continuousOn_invFun
 
 @[simp]
-theorem mk_coe (e : PartialEquiv X Y) (a b) : (PartialHomeomorph.mk e a b : X → Y) = e := rfl
+theorem mk_coe (e : PartialEquiv X Y) (h1 h2) : (PartialHomeomorph.mk e h1 h2 : X → Y) = e := rfl
 
 @[simp]
 theorem mk_coe_symm (e : PartialEquiv X Y) (a b) :
@@ -116,18 +117,18 @@ theorem invFun_eq_coe (e : PartialHomeomorph X Y) : e.invFun = e.symm :=
   rfl
 
 @[simp]
-theorem coe_coe : (e.toPartialEquiv : X → Y) = e :=
+theorem coe_toPartialEquiv : (e.toPartialEquiv : X → Y) = e :=
   rfl
 
 @[simp]
-theorem coe_coe_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
+theorem coe_toPartialEquiv_symm : (e.toPartialEquiv.symm : Y → X) = e.symm :=
   rfl
 
 @[simp]
 theorem map_source {x : X} (h : x ∈ e.source) : e x ∈ e.target :=
   e.map_source' h
 
-/-- Variant of `map_source`, stated for images of subsets of `source`. -/
+/-- Variant of `map_source`, stated in terms of subsets. -/
 lemma map_source'' : e '' e.source ⊆ e.target :=
   fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)
 
@@ -149,7 +150,7 @@ theorem eq_symm_apply {x : X} {y : Y} (hx : x ∈ e.source) (hy : y ∈ e.target
 
 protected theorem mapsTo : MapsTo e e.source e.target := fun _ => e.map_source
 
-protected theorem symm_mapsTo : MapsTo e.symm e.target e.source :=
+protected theorem mapsTo_symm : MapsTo e.symm e.target e.source :=
   e.symm.mapsTo
 
 protected theorem leftInvOn : LeftInvOn e.symm e e.source := fun _ => e.left_inv
@@ -163,7 +164,7 @@ protected theorem injOn : InjOn e e.source :=
   e.leftInvOn.injOn
 
 protected theorem bijOn : BijOn e e.source e.target :=
-  e.invOn.bijOn e.mapsTo e.symm_mapsTo
+  e.invOn.bijOn e.mapsTo e.mapsTo_symm
 
 protected theorem surjOn : SurjOn e e.source e.target :=
   e.bijOn.surjOn