feat: port GroupTheory.Subgroup.Pointwise (#1981)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Feb 1, 2023 · b746237 · b746237
1 parent b937210
commit b746237
Show file tree

Hide file tree

Showing 3 changed files with 562 additions and 8 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -622,6 +622,7 @@ import Mathlib.GroupTheory.Subgroup.Actions
 import Mathlib.GroupTheory.Subgroup.Basic
 import Mathlib.GroupTheory.Subgroup.Finite
 import Mathlib.GroupTheory.Subgroup.MulOpposite
+import Mathlib.GroupTheory.Subgroup.Pointwise
 import Mathlib.GroupTheory.Subgroup.Saturated
 import Mathlib.GroupTheory.Subgroup.Simple
 import Mathlib.GroupTheory.Subgroup.Zpowers

diff --git a/Mathlib/GroupTheory/GroupAction/ConjAct.lean b/Mathlib/GroupTheory/GroupAction/ConjAct.lean
@@ -50,17 +50,13 @@ open MulAction Subgroup
 
 variable {M G G₀ R K}
 
-instance [Group G] : Group (ConjAct G) :=
-  by delta ConjAct; infer_instance
+instance [Group G] : Group (ConjAct G) := ‹Group G›
 
-instance [DivInvMonoid G] : DivInvMonoid (ConjAct G) :=
-  by delta ConjAct; infer_instance
+instance [DivInvMonoid G] : DivInvMonoid (ConjAct G) := ‹DivInvMonoid G›
 
-instance [GroupWithZero G] : GroupWithZero (ConjAct G) :=
-  by delta ConjAct; infer_instance
+instance [GroupWithZero G] : GroupWithZero (ConjAct G) := ‹GroupWithZero G›
 
-instance [Fintype G] : Fintype (ConjAct G) :=
-  by delta ConjAct; infer_instance
+instance [Fintype G] : Fintype (ConjAct G) := ‹Fintype G›
 
 @[simp]
 theorem card [Fintype G] : Fintype.card (ConjAct G) = Fintype.card G :=