diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
index 0859690680279b..681e36f7a7e526 100644
--- a/Mathlib/Geometry/Manifold/ChartedSpace.lean
+++ b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -983,12 +983,9 @@ instance hasGroupoid_continuousGroupoid : HasGroupoid M (continuousGroupoid H) :
 theorem StructureGroupoid.trans_restricted {e e' : PartialHomeomorph M H} {G : StructureGroupoid H}
     (he : e ∈ atlas H M) (he' : e' ∈ atlas H M)
     [HasGroupoid M G] [ClosedUnderRestriction G] (s : Opens M) [Nonempty s] :
-    (e.subtypeRestr s).symm ≫ₕ e'.subtypeRestr s ∈ G := by
-  apply G.eq_on_source ?_ (e.subtypeRestr_symm_trans_subtypeRestr s e')
-  let hopen := e.isOpen_inter_preimage_symm s.2
-  refine G.locality fun x' hx' ↦ ⟨e.target ∩ e.symm ⁻¹' s, hopen, ?_, ?_ ⟩
-  · exact interior_subset (mem_of_mem_inter_right hx')
-  · exact closedUnderRestriction' (closedUnderRestriction' (G.compatible he he') hopen) hopen
+    (e.subtypeRestr s).symm ≫ₕ e'.subtypeRestr s ∈ G :=
+  G.eq_on_source (closedUnderRestriction' (G.compatible he he') (e.isOpen_inter_preimage_symm s.2))
+    (e.subtypeRestr_symm_trans_subtypeRestr s e')
 
 section MaximalAtlas