fix errors

Author: scholzhannah

Mathlib/Geometry/Manifold/IsManifold/Basic.lean

@@ -751,7 +751,7 @@ theorem contDiffGroupoid_prod {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCor
     e.prod e' ∈ contDiffGroupoid n (I.prod I') := by
   obtain ⟨he, he_symm⟩ := he
   obtain ⟨he', he'_symm⟩ := he'
-  constructor <;> simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
+  constructor <;> simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph,
     contDiffPregroupoid]
   · have h3 := ContDiffOn.prodMap he he'
     rw [← I.image_eq, ← I'.image_eq, prod_image_image_eq] at h3

Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean

@@ -228,8 +228,8 @@ lemma prodMap [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsMani
       (domChart_mem_maximalAtlas hf) (domChart_mem_maximalAtlas hg)
   · apply IsManifold.mem_maximalAtlas_prod
       (codChart_mem_maximalAtlas hf) (codChart_mem_maximalAtlas hg)
-  · simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
-      PartialEquiv.prod_source, preimage_prod_map_prod]
+  · simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph, PartialEquiv.prod_source,
+      preimage_prod_map_prod]
     exact prod_mono hf.source_subset_preimage_source hg.source_subset_preimage_source
   · exact h hf.property hg.property
 

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

@@ -248,12 +248,12 @@ variable (K)
 
 theorem expMap_source :
     expMap.source = (Set.univ : Set (realSpace K)) := by
-  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph_toPartialEquiv,
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph,
     PartialEquiv.pi_source, expMap_single, Set.pi_univ Set.univ]
 
 theorem expMap_target :
     expMap.target = Set.univ.pi fun (_ : InfinitePlace K) ↦ Set.Ioi 0 := by
-  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph_toPartialEquiv,
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph,
     PartialEquiv.pi_target, expMap_single]
 
 theorem injective_expMap :