From 4932af45961a169275cbd396801b644a06d61e40 Mon Sep 17 00:00:00 2001
From: qdiazblanco <qdiazblanco@gmail.com>
Date: Fri, 10 Jul 2026 18:34:00 +0200
Subject: [PATCH] Change IsManifold from instance to theorem and put the
 instance after + G now has discrete topology and its own model with corners

---
 .../Geometry/Manifold/Instances/Quotient.lean    | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Geometry/Manifold/Instances/Quotient.lean b/Mathlib/Geometry/Manifold/Instances/Quotient.lean
index ec77d4c99788ca..2beea1a67d55c1 100644
--- a/Mathlib/Geometry/Manifold/Instances/Quotient.lean
+++ b/Mathlib/Geometry/Manifold/Instances/Quotient.lean
@@ -179,9 +179,11 @@ lemma StructureGroupoid.restr_mem_of_eqOn {G : StructureGroupoid X}
 end
 
 -- the action is smooth
-variable [TopologicalSpace G] [ChartedSpace H G] [ContMDiffSMul I I n G M]
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H' : Type*}
+  [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace G] [ChartedSpace H' G]
 
-instance : IsManifold I n (orbitRel.Quotient G M) where
+theorem isManifold_quotient_of_contMDiffSMul [ContMDiffSMul J I n G M] :
+    IsManifold  I n (orbitRel.Quotient G M) where
   compatible := by
     rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
     rw [(πinv x).trans_symm_eq_symm_trans_symm, (chartAt H x.out).symm.trans_assoc,
@@ -197,12 +199,18 @@ instance : IsManifold I n (orbitRel.Quotient G M) where
     refine StructureGroupoid.restr_mem_of_eqOn (mem_contDiffGroupoid_of_contMDiff_chartAt I ?_ ?_)
       hto (hg0'.mono inter_subset_right) ?_
     · rw [Homeomorph.toOpenPartialHomeomorph_apply]
-      exact ContMDiffSMul.contMDiff_const_smul (I := I) g0
+      exact ContMDiffSMul.contMDiff_const_smul (I := J) g0
     · rw [Homeomorph.toOpenPartialHomeomorph_symm_apply]
-      exact ContMDiffSMul.contMDiff_const_smul (I := I) g0⁻¹
+      exact ContMDiffSMul.contMDiff_const_smul (I := J) g0⁻¹
     · rintro h' ⟨⟨hQ1, _, hQ4⟩, _, hcert⟩
       exact ⟨hQ1, mem_univ _, by simpa [← smul_eqOn x y g0 hcert] using hQ4⟩
 
+open scoped Manifold
+
+attribute [local instance] ChartedSpace.of_discreteTopology
+instance [DiscreteTopology G] [ContMDiffSMul 𝓘(𝕜, PUnit) I n G M] :
+    IsManifold I n (orbitRel.Quotient G M) := isManifold_quotient_of_contMDiffSMul I 𝓘(𝕜, PUnit)
+
 end MulAction
 
 end