From 7687a277e6912678615d9d76c08fb85f8be1d1f2 Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Thu, 22 Jun 2023 23:07:58 +0000
Subject: [PATCH] chore: forward port leanprover-community/mathlib#19146
 (#5371)

---
 Mathlib/Geometry/Manifold/ChartedSpace.lean   | 16 +++++++++-
 .../Manifold/LocalInvariantProperties.lean    | 24 ++++++++++++--
 Mathlib/Topology/LocalHomeomorph.lean         | 31 ++++++++++++++++++-
 3 files changed, 67 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
index 70d8552b0eea6..69168787af1f6 100644
--- a/Mathlib/Geometry/Manifold/ChartedSpace.lean
+++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module geometry.manifold.charted_space
-! leanprover-community/mathlib commit bcfa726826abd57587355b4b5b7e78ad6527b7e4
+! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1080,6 +1080,20 @@ protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G
     · exact preimage_open_of_open_symm (chartAt _ _) s.2
 #align topological_space.opens.has_groupoid TopologicalSpace.Opens.instHasGroupoid
 
+theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
+    (chartAt H (Set.inclusion hUV x)).symm
+    =ᶠ[𝓝 (chartAt H (Set.inclusion hUV x) (Set.inclusion hUV x))]
+    Set.inclusion hUV ∘ (chartAt H x).symm := by
+  set i := Set.inclusion hUV
+  set e := chartAt H (x : M)
+  haveI : Nonempty U := ⟨x⟩
+  haveI : Nonempty V := ⟨i x⟩
+  have heUx_nhds : (e.subtypeRestr U).target ∈ 𝓝 (e x) := by
+    apply (e.subtypeRestr U).open_target.mem_nhds
+    exact e.map_subtype_source (mem_chart_source _ _)
+  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn_of_le hUV)
+#align topological_space.opens.chart_at_inclusion_symm_eventually_eq TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq
+
 end TopologicalSpace.Opens
 
 /-! ### Structomorphisms -/
diff --git a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
index c405e445d77c7..f1cd5f3cf9620 100644
--- a/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
+++ b/Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn
 
 ! This file was ported from Lean 3 source module geometry.manifold.local_invariant_properties
-! leanprover-community/mathlib commit be2c24f56783935652cefffb4bfca7e4b25d167e
+! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -52,7 +52,7 @@ noncomputable section
 
 open Classical Manifold Topology
 
-open Set Filter
+open Set Filter TopologicalSpace
 
 variable {H M H' M' X : Type _}
 
@@ -545,6 +545,26 @@ theorem liftProp_id (hG : G.LocalInvariantProp G Q) (hQ : ∀ y, Q id univ y) :
   exact fun x ↦ hG.congr' ((chartAt H x).eventually_right_inverse <| mem_chart_target H x) (hQ _)
 #align structure_groupoid.local_invariant_prop.lift_prop_id StructureGroupoid.LocalInvariantProp.liftProp_id
 
+theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V)
+    (f : V → M') (x : U) :
+    LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by
+  change (_ ∧ _) ↔ (_ ∧ _); congr! 1 -- Porting note: was `congrm _ ∧ _`
+  · simp [continuousWithinAt_univ,
+      (TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff]
+  · apply hG.congr_iff
+    exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp
+      (chartAt H' (f (Set.inclusion hUV x)) ∘ f)
+#align structure_groupoid.local_invariant_prop.lift_prop_at_iff_comp_inclusion StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion
+
+theorem liftProp_inclusion {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q)
+    (hQ : ∀ y, Q id univ y) {U V : Opens M} (hUV : U ≤ V) :
+    LiftProp Q (Set.inclusion hUV : U → V) := by
+  intro x
+  show LiftPropAt Q (id ∘ inclusion hUV) x
+  rw [← hG.liftPropAt_iff_comp_inclusion hUV]
+  apply hG.liftProp_id hQ
+#align structure_groupoid.local_invariant_prop.lift_prop_inclusion StructureGroupoid.LocalInvariantProp.liftProp_inclusion
+
 end LocalInvariantProp
 
 section LocalStructomorph
diff --git a/Mathlib/Topology/LocalHomeomorph.lean b/Mathlib/Topology/LocalHomeomorph.lean
index 76759ab1fa2aa..6260c6f92fd5a 100644
--- a/Mathlib/Topology/LocalHomeomorph.lean
+++ b/Mathlib/Topology/LocalHomeomorph.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 
 ! This file was ported from Lean 3 source module topology.local_homeomorph
-! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! leanprover-community/mathlib commit 431589bce478b2229eba14b14a283250428217db
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1379,6 +1379,16 @@ theorem subtypeRestr_source : (e.subtypeRestr s).source = (↑) ⁻¹' e.source
   simp only [subtypeRestr_def, mfld_simps]
 #align local_homeomorph.subtype_restr_source LocalHomeomorph.subtypeRestr_source
 
+variable {s}
+
+theorem map_subtype_source {x : s} (hxe : (x : α) ∈ e.source): e x ∈ (e.subtypeRestr s).target := by
+  refine' ⟨e.map_source hxe, _⟩
+  rw [s.localHomeomorphSubtypeCoe_target, mem_preimage, e.leftInvOn hxe]
+  exact x.prop
+#align local_homeomorph.map_subtype_source LocalHomeomorph.map_subtype_source
+
+variable (s)
+
 /- This lemma characterizes the transition functions of an open subset in terms of the transition
 functions of the original space. -/
 theorem subtypeRestr_symm_trans_subtypeRestr (f f' : LocalHomeomorph α β) :
@@ -1399,4 +1409,23 @@ theorem subtypeRestr_symm_trans_subtypeRestr (f f' : LocalHomeomorph α β) :
   simp only [mfld_simps, Setoid.refl]
 #align local_homeomorph.subtype_restr_symm_trans_subtype_restr LocalHomeomorph.subtypeRestr_symm_trans_subtypeRestr
 
+theorem subtypeRestr_symm_eqOn_of_le {U V : Opens α} [Nonempty U] [Nonempty V] (hUV : U ≤ V) :
+    EqOn (e.subtypeRestr V).symm (Set.inclusion hUV ∘ (e.subtypeRestr U).symm)
+      (e.subtypeRestr U).target := by
+  set i := Set.inclusion hUV
+  intro y hy
+  dsimp [LocalHomeomorph.subtypeRestr_def] at hy ⊢
+  have hyV : e.symm y ∈ V.localHomeomorphSubtypeCoe.target := by
+    rw [Opens.localHomeomorphSubtypeCoe_target] at hy ⊢
+    exact hUV hy.2
+  refine' V.localHomeomorphSubtypeCoe.injOn _ trivial _
+  · rw [← LocalHomeomorph.symm_target]
+    apply LocalHomeomorph.map_source
+    rw [LocalHomeomorph.symm_source]
+    exact hyV
+  · rw [V.localHomeomorphSubtypeCoe.right_inv hyV]
+    show _ = U.localHomeomorphSubtypeCoe _
+    rw [U.localHomeomorphSubtypeCoe.right_inv hy.2]
+#align local_homeomorph.subtype_restr_symm_eq_on_of_le LocalHomeomorph.subtypeRestr_symm_eqOn_of_le
+
 end LocalHomeomorph