fix errors

Author: scholzhannah

Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

@@ -455,7 +455,8 @@ lemma contMDiff_equivTangentBundleProd_symm :
     filter_upwards [chart_source_mem_nhds (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)]
       with p hp
     -- now we have to check that the original map coincides locally with `pM` read in target chart.
-    simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
+    simp only [prodChartedSpace_chartAt,
+      OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
       PartialEquiv.prod_source, mem_prod, TangentBundle.mem_chart_source_iff] at hp
     let φ (x : E) := I ((chartAt H a.proj) ((chartAt H p.1.proj).symm (I.symm x)))
     have D0 : DifferentiableWithinAt 𝕜 φ (Set.range I) (I ((chartAt H p.1.proj) p.1.proj)) := by
@@ -494,7 +495,8 @@ lemma contMDiff_equivTangentBundleProd_symm :
     filter_upwards [chart_source_mem_nhds (ModelProd (ModelProd H E) (ModelProd H' E')) (a, b)]
       with p hp
     -- now we have to check that the original map coincides locally with `pM'` read in target chart.
-    simp only [prodChartedSpace_chartAt, OpenPartialHomeomorph.prod_toPartialEquiv,
+    simp only [prodChartedSpace_chartAt,
+      OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
       PartialEquiv.prod_source, mem_prod, TangentBundle.mem_chart_source_iff] at hp
     let φ (x : E') := I' ((chartAt H' b.proj) ((chartAt H' p.2.proj).symm (I'.symm x)))
     have D0 : DifferentiableWithinAt 𝕜 φ (Set.range I') (I' ((chartAt H' p.2.proj) p.2.proj)) := by

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 [PartialEquiv.prod_source, OpenPartialHomeomorph.prod_toPartialEquiv,
+  constructor <;> simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
     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_toPartialEquiv, PartialEquiv.prod_source,
-      preimage_prod_map_prod]
+  · simp only [OpenPartialHomeomorph.prod_toPartialHomeomorph_toPartialEquiv,
+      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,13 @@ variable (K)
 
 theorem expMap_source :
     expMap.source = (Set.univ : Set (realSpace K)) := by
-  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialEquiv, PartialEquiv.pi_source, expMap_single,
-    Set.pi_univ Set.univ]
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph_toPartialEquiv,
+    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_toPartialEquiv, PartialEquiv.pi_target, expMap_single]
+  simp_rw [expMap, OpenPartialHomeomorph.pi_toPartialHomeomorph_toPartialEquiv,
+    PartialEquiv.pi_target, expMap_single]
 
 theorem injective_expMap :
     Function.Injective (expMap : realSpace K → realSpace K) :=

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -412,8 +412,9 @@ initialize_simps_projections Trivialization (toFun → apply, invFun → symm_ap
 theorem toPretrivialization_injective :
     Function.Injective fun e : Trivialization F proj => e.toPretrivialization := fun e e' h => by
   ext1
-  exacts [OpenPartialHomeomorph.toPartialEquiv_injective
-    (congr_arg Pretrivialization.toPartialEquiv h), congr_arg Pretrivialization.baseSet h]
+  exacts [OpenPartialHomeomorph.toPartialHomeomorph_injective
+    (PartialHomeomorph.toPartialEquiv_injective (congr_arg Pretrivialization.toPartialEquiv h)),
+    congr_arg Pretrivialization.baseSet h]
 
 @[simp, mfld_simps]
 theorem coe_coe : ⇑e.toOpenPartialHomeomorph = e :=