diff --git a/src/algebra/algebra/operations.lean b/src/algebra/algebra/operations.lean
index 0aed542473aac..e4005a9327f7b 100644
--- a/src/algebra/algebra/operations.lean
+++ b/src/algebra/algebra/operations.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import algebra.algebra.basic
+import algebra.module.submodule_pointwise
 
 /-!
 # Multiplication and division of submodules of an algebra.
diff --git a/src/algebra/category/Group/limits.lean b/src/algebra/category/Group/limits.lean
index b73b23bc4bc3c..0bca8734f6059 100644
--- a/src/algebra/category/Group/limits.lean
+++ b/src/algebra/category/Group/limits.lean
@@ -8,7 +8,7 @@ import algebra.category.Group.preadditive
 import category_theory.over
 import category_theory.limits.concrete_category
 import category_theory.limits.shapes.concrete_category
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # The category of (commutative) (additive) groups has all limits
diff --git a/src/algebra/direct_sum/basic.lean b/src/algebra/direct_sum/basic.lean
index 40561e1af3d38..73f20c85055bc 100644
--- a/src/algebra/direct_sum/basic.lean
+++ b/src/algebra/direct_sum/basic.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau
 -/
 import data.dfinsupp
 import group_theory.submonoid.operations
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Direct sum
diff --git a/src/algebra/direct_sum/ring.lean b/src/algebra/direct_sum/ring.lean
index e4097dcbdf8eb..8d6a415a8ad61 100644
--- a/src/algebra/direct_sum/ring.lean
+++ b/src/algebra/direct_sum/ring.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import algebra.algebra.basic
 import algebra.algebra.operations
 import algebra.direct_sum.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Additively-graded multiplicative structures on `⨁ i, A i`
diff --git a/src/algebra/group_ring_action.lean b/src/algebra/group_ring_action.lean
index aad48879b09ba..7ed2ab9e53ee3 100644
--- a/src/algebra/group_ring_action.lean
+++ b/src/algebra/group_ring_action.lean
@@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
-import group_theory.group_action.group
+import algebra.pointwise
 import data.equiv.ring
+import group_theory.group_action.group
+import group_theory.submonoid.pointwise
+import group_theory.subgroup.pointwise
 import ring_theory.subring
-import algebra.pointwise
 
 /-!
 # Group action on rings
diff --git a/src/algebra/module/submodule_pointwise.lean b/src/algebra/module/submodule_pointwise.lean
new file mode 100644
index 0000000000000..6329639c12568
--- /dev/null
+++ b/src/algebra/module/submodule_pointwise.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import group_theory.subgroup.pointwise
+import linear_algebra.basic
+
+/-! # Pointwise instances on `submodule`s
+
+This file provides the actions
+
+* `submodule.pointwise_distrib_mul_action`
+* `submodule.pointwise_mul_action_with_zero`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+-/
+
+namespace submodule
+
+variables {α : Type*} {R : Type*} {M : Type*}
+variables [semiring R] [add_comm_monoid M] [module R M]
+
+
+instance pointwise_add_comm_monoid : add_comm_monoid (submodule R M) :=
+{ add := (⊔),
+  add_assoc := λ _ _ _, sup_assoc,
+  zero := ⊥,
+  zero_add := λ _, bot_sup_eq,
+  add_zero := λ _, sup_bot_eq,
+  add_comm := λ _ _, sup_comm }
+
+@[simp] lemma add_eq_sup (p q : submodule R M) : p + q = p ⊔ q := rfl
+@[simp] lemma zero_eq_bot : (0 : submodule R M) = ⊥ := rfl
+
+
+section
+variables [monoid α] [distrib_mul_action α M] [smul_comm_class α R M]
+
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_distrib_mul_action : distrib_mul_action α (submodule R M) :=
+{ smul := λ a S, S.map (distrib_mul_action.to_linear_map _ _ a),
+  one_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact one_smul α)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact mul_smul _ _)).trans (S.map_comp _ _),
+  smul_zero := λ a, map_bot _,
+  smul_add := λ a S₁ S₂, map_sup _ _ _ }
+
+localized "attribute [instance] submodule.pointwise_distrib_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : submodule R M) : ↑(a • S) = a • (S : set M) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : submodule R M) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+@[simp] lemma pointwise_smul_to_add_subgroup {R M : Type*}
+  [ring R] [add_comm_group M] [distrib_mul_action α M] [module R M] [smul_comm_class α R M]
+  (a : α) (S : submodule R M) :
+  (a • S).to_add_subgroup = a • S.to_add_subgroup := rfl
+
+lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
+
+@[simp] lemma smul_le_self_of_tower {α : Type*}
+  [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
+  (a : α) (S : submodule R M) : a • S ≤ S :=
+begin
+  rintro y ⟨x, hx, rfl⟩,
+  exact smul_of_tower_mem _ a hx,
+end
+
+end
+
+section
+variables [semiring α] [module α M] [smul_comm_class α R M]
+/-- The action on a submodule corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale.
+
+This is a stronger version of `submodule.pointwise_distrib_mul_action`. Note that `add_smul` does
+not hold so this cannot be stated as a `module`. -/
+protected def pointwise_mul_action_with_zero : mul_action_with_zero α (submodule R M) :=
+{ zero_smul := λ S,
+    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact zero_smul α)).trans S.map_zero,
+  .. submodule.pointwise_distrib_mul_action }
+
+localized "attribute [instance] submodule.pointwise_mul_action_with_zero" in pointwise
+
+end
+
+end submodule
diff --git a/src/deprecated/subgroup.lean b/src/deprecated/subgroup.lean
index ecb28b28479bd..d44481cb73614 100644
--- a/src/deprecated/subgroup.lean
+++ b/src/deprecated/subgroup.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro,
   Michael Howes
 -/
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import deprecated.submonoid
 /-!
 # Unbundled subgroups
diff --git a/src/group_theory/archimedean.lean b/src/group_theory/archimedean.lean
index 25b11da804a7c..1aba4767f1244 100644
--- a/src/group_theory/archimedean.lean
+++ b/src/group_theory/archimedean.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Heather Macbeth, Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, Patrick Massot
 -/
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import algebra.archimedean
 
 /-!
diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
index 49b88a247295d..bc6d48fe1c0fd 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mitchell Rowett, Scott Morrison
 -/
 
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Cosets
diff --git a/src/group_theory/finiteness.lean b/src/group_theory/finiteness.lean
index b94a20928c61a..3c753586285a8 100644
--- a/src/group_theory/finiteness.lean
+++ b/src/group_theory/finiteness.lean
@@ -6,7 +6,7 @@ Authors: Riccardo Brasca
 
 import data.set.finite
 import group_theory.submonoid.operations
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Finitely generated monoids and groups
diff --git a/src/group_theory/free_group.lean b/src/group_theory/free_group.lean
index 6130964011e10..49bb030f01cbd 100644
--- a/src/group_theory/free_group.lean
+++ b/src/group_theory/free_group.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import data.fintype.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Free groups
diff --git a/src/group_theory/general_commutator.lean b/src/group_theory/general_commutator.lean
index 59cef90c874b1..40b8af50f46d0 100644
--- a/src/group_theory/general_commutator.lean
+++ b/src/group_theory/general_commutator.lean
@@ -5,7 +5,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
 
 import data.bracket
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import tactic.group
 
 /-!
diff --git a/src/group_theory/perm/subgroup.lean b/src/group_theory/perm/subgroup.lean
index f3fa16a6f2784..740de3bd942c7 100644
--- a/src/group_theory/perm/subgroup.lean
+++ b/src/group_theory/perm/subgroup.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import group_theory.perm.basic
 import data.fintype.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 /-!
 # Lemmas about subgroups within the permutations (self-equivalences) of a type `α`
 
diff --git a/src/group_theory/semidirect_product.lean b/src/group_theory/semidirect_product.lean
index 35cff2d99bf26..720c550b02df6 100644
--- a/src/group_theory/semidirect_product.lean
+++ b/src/group_theory/semidirect_product.lean
@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import data.equiv.mul_add_aut
 import logic.function.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Semidirect product
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup/basic.lean
similarity index 97%
rename from src/group_theory/subgroup.lean
rename to src/group_theory/subgroup/basic.lean
index 92a42a2f2890e..b9a3d921b697c 100644
--- a/src/group_theory/subgroup.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -5,9 +5,7 @@ Authors: Kexing Ying
 -/
 import group_theory.submonoid
 import group_theory.submonoid.center
-import group_theory.submonoid.pointwise
 import algebra.group.conj
-import algebra.pointwise
 import order.atoms
 
 /-!
@@ -2339,65 +2337,6 @@ end subgroup
 
 end actions
 
-/-! ### Pointwise instances on `subgroup`s -/
-
-section
-variables {α : Type*}
-
-namespace subgroup
-
-variables [monoid α] [mul_distrib_mul_action α G]
-
-/-- The action on a subgroup corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (subgroup G) :=
-{ smul := λ a S, S.map (mul_distrib_mul_action.to_monoid_End _ _ a),
-  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
-
-localized "attribute [instance] subgroup.pointwise_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (a : α) (S : subgroup G) : ↑(a • S) = a • (S : set G) := rfl
-
-@[simp] lemma pointwise_smul_to_submonoid (a : α) (S : subgroup G) :
-  (a • S).to_submonoid = a • S.to_submonoid := rfl
-
-lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
-
-end subgroup
-
-namespace add_subgroup
-
-variables [monoid α] [distrib_mul_action α A]
-
-/-- The action on a additive subgroup corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_mul_action : mul_action α (add_subgroup A) :=
-{ smul := λ a S, S.map (distrib_mul_action.to_add_monoid_End _ _ a),
-  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
-
-localized "attribute [instance] add_subgroup.pointwise_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (a : α) (S : add_subgroup A) : ↑(a • S) = a • (S : set A) := rfl
-
-@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : add_subgroup A) :
-  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
-
-lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
-
-end add_subgroup
-
-end
-
 /-! ### Saturated subgroups -/
 
 section saturated
diff --git a/src/group_theory/subgroup/pointwise.lean b/src/group_theory/subgroup/pointwise.lean
new file mode 100644
index 0000000000000..453db913951be
--- /dev/null
+++ b/src/group_theory/subgroup/pointwise.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import group_theory.subgroup.basic
+import group_theory.submonoid.pointwise
+
+/-! # Pointwise instances on `subgroup`s
+
+This file provides the actions
+
+* `subgroup.pointwise_mul_action`
+* `add_subgroup.pointwise_mul_action`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+-/
+
+variables {α : Type*} {G : Type*} {A : Type*} [group G] [add_group A]
+
+namespace subgroup
+
+variables [monoid α] [mul_distrib_mul_action α G]
+
+/-- The action on a subgroup corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_mul_action : mul_action α (subgroup G) :=
+{ smul := λ a S, S.map (mul_distrib_mul_action.to_monoid_End _ _ a),
+  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : subgroup G) : ↑(a • S) = a • (S : set G) := rfl
+
+@[simp] lemma pointwise_smul_to_submonoid (a : α) (S : subgroup G) :
+  (a • S).to_submonoid = a • S.to_submonoid := rfl
+
+lemma smul_mem_pointwise_smul (m : G) (a : α) (S : subgroup G) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set G))
+
+end subgroup
+
+namespace add_subgroup
+
+variables [monoid α] [distrib_mul_action α A]
+
+/-- The action on a additive subgroup corresponding to applying the action to every element.
+
+This is available as an instance in the `pointwise` locale. -/
+protected def pointwise_mul_action : mul_action α (add_subgroup A) :=
+{ smul := λ a S, S.map (distrib_mul_action.to_add_monoid_End _ _ a),
+  one_smul := λ S, (congr_arg (λ f, S.map f) (monoid_hom.map_one _)).trans S.map_id,
+  mul_smul := λ a₁ a₂ S,
+    (congr_arg (λ f, S.map f) (monoid_hom.map_mul _ _ _)).trans (S.map_map _ _).symm,}
+
+localized "attribute [instance] add_subgroup.pointwise_mul_action" in pointwise
+open_locale pointwise
+
+@[simp] lemma coe_pointwise_smul (a : α) (S : add_subgroup A) : ↑(a • S) = a • (S : set A) := rfl
+
+@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : add_subgroup A) :
+  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
+
+lemma smul_mem_pointwise_smul (m : A) (a : α) (S : add_subgroup A) : m ∈ S → a • m ∈ a • S :=
+(set.smul_mem_smul_set : _ → _ ∈ a • (S : set A))
+
+end add_subgroup
diff --git a/src/group_theory/submonoid/pointwise.lean b/src/group_theory/submonoid/pointwise.lean
index f6c956d5139ec..6bc4c09f1eb48 100644
--- a/src/group_theory/submonoid/pointwise.lean
+++ b/src/group_theory/submonoid/pointwise.lean
@@ -6,7 +6,18 @@ Authors: Eric Wieser
 import group_theory.submonoid.operations
 import algebra.pointwise
 
-/-! ### Pointwise instances on `submonoid`s and `add_submonoid`s -/
+/-! # Pointwise instances on `submonoid`s and `add_submonoid`s
+
+This file provides the actions
+
+* `submonoid.pointwise_mul_action`
+* `add_submonoid.pointwise_mul_action`
+
+which matches the action of `mul_action_set`.
+
+These actions are available in the `pointwise` locale.
+
+-/
 
 section
 variables {M' : Type*} {α β : Type*}
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index d56b8bd4e9201..89efbb3e3a0a1 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -696,18 +696,6 @@ lemma subtype_comp_of_le (p q : submodule R M) (h : p ≤ q) :
   q.subtype.comp (of_le h) = p.subtype :=
 by { ext ⟨b, hb⟩, refl }
 
-
-instance pointwise_add_comm_monoid : add_comm_monoid (submodule R M) :=
-{ add := (⊔),
-  add_assoc := λ _ _ _, sup_assoc,
-  zero := ⊥,
-  zero_add := λ _, bot_sup_eq,
-  add_zero := λ _, sup_bot_eq,
-  add_comm := λ _ _, sup_comm }
-
-@[simp] lemma add_eq_sup (p q : submodule R M) : p + q = p ⊔ q := rfl
-@[simp] lemma zero_eq_bot : (0 : submodule R M) = ⊥ := rfl
-
 variables (R)
 
 @[simp] lemma subsingleton_iff : subsingleton (submodule R M) ↔ subsingleton M :=
@@ -780,7 +768,7 @@ image_subset _
 have ∃ (x : M), x ∈ p := ⟨0, p.zero_mem⟩,
 ext $ by simp [this, eq_comm]
 
-lemma map_add_le (f g : M →ₗ[R] M₂) : map (f + g) p ≤ map f p + map g p :=
+lemma map_add_le (f g : M →ₗ[R] M₂) : map (f + g) p ≤ map f p ⊔ map g p :=
 begin
   rintros x ⟨m, hm, rfl⟩,
   exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm),
@@ -951,65 +939,6 @@ ext $ λ x, ⟨by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩,
 lemma eq_zero_of_bot_submodule : ∀(b : (⊥ : submodule R M)), b = 0
 | ⟨b', hb⟩ := subtype.eq $ show b' = 0, from (mem_bot R).1 hb
 
-
-section
-variables {α : Type*} [monoid α] [distrib_mul_action α M] [smul_comm_class α R M]
-
-/-- The action on a submodule corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale. -/
-protected def pointwise_distrib_mul_action : distrib_mul_action α (submodule R M) :=
-{ smul := λ a S, S.map (distrib_mul_action.to_linear_map _ _ a),
-  one_smul := λ S,
-    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact one_smul α)).trans S.map_id,
-  mul_smul := λ a₁ a₂ S,
-    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact mul_smul _ _)).trans (S.map_comp _ _),
-  smul_zero := λ a, map_bot _,
-  smul_add := λ a S₁ S₂, map_sup _ _ _ }
-
-localized "attribute [instance] submodule.pointwise_distrib_mul_action" in pointwise
-open_locale pointwise
-
-@[simp] lemma coe_pointwise_smul (a : α) (S : submodule R M) : ↑(a • S) = a • (S : set M) := rfl
-
-@[simp] lemma pointwise_smul_to_add_submonoid (a : α) (S : submodule R M) :
-  (a • S).to_add_submonoid = a • S.to_add_submonoid := rfl
-
-@[simp] lemma pointwise_smul_to_add_subgroup {R M : Type*}
-  [ring R] [add_comm_group M] [distrib_mul_action α M] [module R M] [smul_comm_class α R M]
-  (a : α) (S : submodule R M) :
-  (a • S).to_add_subgroup = a • S.to_add_subgroup := rfl
-
-lemma smul_mem_pointwise_smul (m : M) (a : α) (S : submodule R M) : m ∈ S → a • m ∈ a • S :=
-(set.smul_mem_smul_set : _ → _ ∈ a • (S : set M))
-
-@[simp] lemma smul_le_self_of_tower {α : Type*}
-  [semiring α] [module α R] [module α M] [smul_comm_class α R M] [is_scalar_tower α R M]
-  (a : α) (S : submodule R M) : a • S ≤ S :=
-begin
-  rintro y ⟨x, hx, rfl⟩,
-  exact smul_of_tower_mem _ a hx,
-end
-
-end
-
-section
-variables {α : Type*} [semiring α] [module α M] [smul_comm_class α R M]
-/-- The action on a submodule corresponding to applying the action to every element.
-
-This is available as an instance in the `pointwise` locale.
-
-This is a stronger version of `submodule.pointwise_distrib_mul_action`. Note that `add_smul` does
-not hold so this cannot be stated as a `module`. -/
-protected def pointwise_mul_action_with_zero : mul_action_with_zero α (submodule R M) :=
-{ zero_smul := λ S,
-    (congr_arg (λ f, S.map f) (linear_map.ext $ by exact zero_smul α)).trans S.map_zero,
-  .. submodule.pointwise_distrib_mul_action }
-
-localized "attribute [instance] submodule.pointwise_mul_action_with_zero" in pointwise
-
-end
-
 section
 variables (R)
 
@@ -1330,13 +1259,13 @@ instance : is_compactly_generated (submodule R M) :=
   apply singleton_span_is_compact_element,
 end, by rw [Sup_eq_supr, supr_image, ←span_eq_supr_of_singleton_spans, span_eq]⟩⟩⟩
 
-lemma lt_add_iff_not_mem {I : submodule R M} {a : M} : I < I + (R ∙ a) ↔ a ∉ I :=
+lemma lt_sup_iff_not_mem {I : submodule R M} {a : M} : I < I ⊔ (R ∙ a) ↔ a ∉ I :=
 begin
   split,
   { intro h,
     by_contra akey,
-    have h1 : I + (R ∙ a) ≤ I,
-    { simp only [add_eq_sup, sup_le_iff],
+    have h1 : I ⊔ (R ∙ a) ≤ I,
+    { simp only [sup_le_iff],
       split,
       { exact le_refl I, },
       { exact (span_singleton_le_iff_mem a I).mpr akey, } },
@@ -1344,10 +1273,10 @@ begin
     exact lt_irrefl I h2, },
   { intro h,
     apply set_like.lt_iff_le_and_exists.mpr, split,
-    simp only [add_eq_sup, le_sup_left],
+    simp only [le_sup_left],
     use a,
     split, swap, { assumption, },
-    { have : (R ∙ a) ≤ I + (R ∙ a) := le_sup_right,
+    { have : (R ∙ a) ≤ I ⊔ (R ∙ a) := le_sup_right,
       exact this (mem_span_singleton_self a), } },
 end
 
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index 89a2877fa5d3a..8d62c3bf832b4 100644
--- a/src/ring_theory/subring.lean
+++ b/src/ring_theory/subring.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan
 -/
 
-import group_theory.subgroup
+import group_theory.subgroup.basic
 import ring_theory.subsemiring
 
 /-!
diff --git a/src/topology/algebra/nonarchimedean/basic.lean b/src/topology/algebra/nonarchimedean/basic.lean
index 118fc5918e652..1ee2fdc6957f2 100644
--- a/src/topology/algebra/nonarchimedean/basic.lean
+++ b/src/topology/algebra/nonarchimedean/basic.lean
@@ -6,7 +6,7 @@ Authors: Kevin Buzzard, Johan Commelin, Ashwin Iyengar, Patrick Massot
 import topology.algebra.ring
 import topology.algebra.open_subgroup
 import data.set.basic
-import group_theory.subgroup
+import group_theory.subgroup.basic
 
 /-!
 # Nonarchimedean Topology