diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
index a003f4797c200..b9d3ea1d22334 100644
--- a/src/algebra/algebra/basic.lean
+++ b/src/algebra/algebra/basic.lean
@@ -1510,7 +1510,7 @@ lemma span_eq_restrict_scalars (X : set M) (hsur : function.surjective (algebra_
   span R X = restrict_scalars R (span A X) :=
 begin
   apply (span_le_restrict_scalars R A X).antisymm (λ m hm, _),
-  refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem _) (λ a m hm, _),
+  refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem) (λ a m hm, _),
   obtain ⟨r, rfl⟩ := hsur a,
   simpa [algebra_map_smul] using smul_mem _ r hm
 end
diff --git a/src/algebra/algebra/operations.lean b/src/algebra/algebra/operations.lean
index 8ae0cbedec9cc..12fe8dc2ee777 100644
--- a/src/algebra/algebra/operations.lean
+++ b/src/algebra/algebra/operations.lean
@@ -121,7 +121,7 @@ end
 @[elab_as_eliminator] protected theorem mul_induction_on'
   {C : Π r, r ∈ M * N → Prop}
   (hm : ∀ (m ∈ M) (n ∈ N), C (m * n) (mul_mem_mul ‹_› ‹_›))
-  (ha : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem _ ‹_› ‹_›))
+  (ha : ∀ x hx y hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›))
   {r : A} (hr : r ∈ M * N) : C r hr :=
 begin
   refine exists.elim _ (λ (hr : r ∈ M * N) (hc : C r hr), hc),
@@ -139,7 +139,8 @@ begin
       work_on_goal 1 { intros, exact subset_span ⟨_, _, ‹_›, ‹_›, rfl⟩ } },
     all_goals { intros, simp only [mul_zero, zero_mul, zero_mem,
         left_distrib, right_distrib, mul_smul_comm, smul_mul_assoc],
-      try {apply add_mem _ _ _}, try {apply smul_mem _ _ _} }, assumption' },
+      solve_by_elim [add_mem _ _, zero_mem _, smul_mem _ _ _]
+        { max_depth := 4, discharger := tactic.interactive.apply_instance } } },
   { rw span_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
     exact mul_mem_mul (subset_span ha) (subset_span hb) }
 end
@@ -357,7 +358,7 @@ end
 @[elab_as_eliminator] protected theorem pow_induction_on'
   {C : Π (n : ℕ) x, x ∈ M ^ n → Prop}
   (hr : ∀ r : R, C 0 (algebra_map _ _ r) (algebra_map_mem r))
-  (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem _ ‹_› ‹_›))
+  (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem ‹_› ‹_›))
   (hmul : ∀ (m ∈ M) i x hx, C i x hx → C (i.succ) (m * x) (mul_mem_mul H hx))
   {x : A} {n : ℕ} (hx : x ∈ M ^ n) : C n x hx :=
 begin
diff --git a/src/algebra/algebra/subalgebra/basic.lean b/src/algebra/algebra/subalgebra/basic.lean
index 8671d9f987f14..11db8db83deaf 100644
--- a/src/algebra/algebra/subalgebra/basic.lean
+++ b/src/algebra/algebra/subalgebra/basic.lean
@@ -90,72 +90,49 @@ theorem range_subset : set.range (algebra_map R A) ⊆ S :=
 theorem range_le : set.range (algebra_map R A) ≤ S :=
 S.range_subset
 
-theorem one_mem : (1 : A) ∈ S :=
-S.to_subsemiring.one_mem
-
-theorem mul_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S :=
-S.to_subsemiring.mul_mem hx hy
-
 theorem smul_mem {x : A} (hx : x ∈ S) (r : R) : r • x ∈ S :=
-(algebra.smul_def r x).symm ▸ S.mul_mem (S.algebra_map_mem r) hx
-
-theorem pow_mem {x : A} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
-S.to_subsemiring.pow_mem hx n
-
-theorem zero_mem : (0 : A) ∈ S :=
-S.to_subsemiring.zero_mem
-
-theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S :=
-S.to_subsemiring.add_mem hx hy
+(algebra.smul_def r x).symm ▸ mul_mem (S.algebra_map_mem r) hx
+
+protected theorem one_mem : (1 : A) ∈ S := one_mem S
+protected theorem mul_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x * y ∈ S := mul_mem hx hy
+protected theorem pow_mem {x : A} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S := pow_mem hx n
+protected theorem zero_mem : (0 : A) ∈ S := zero_mem S
+protected theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S := add_mem hx hy
+protected theorem nsmul_mem {x : A} (hx : x ∈ S) (n : ℕ) : n • x ∈ S := nsmul_mem hx n
+protected theorem coe_nat_mem (n : ℕ) : (n : A) ∈ S := coe_nat_mem S n
+protected theorem list_prod_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S := list_prod_mem h
+protected theorem list_sum_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.sum ∈ S := list_sum_mem h
+protected theorem multiset_sum_mem {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S :=
+multiset_sum_mem m h
+protected theorem sum_mem {ι : Type w} {t : finset ι} {f : ι → A} (h : ∀ x ∈ t, f x ∈ S) :
+  ∑ x in t, f x ∈ S :=
+sum_mem h
+
+protected theorem multiset_prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
+  [algebra R A] (S : subalgebra R A) {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.prod ∈ S :=
+multiset_prod_mem m h
+protected theorem prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
+  [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A}
+  (h : ∀ x ∈ t, f x ∈ S) : ∏ x in t, f x ∈ S :=
+prod_mem h
 
 instance {R A : Type*} [comm_ring R] [ring A] [algebra R A] : subring_class (subalgebra R A) A :=
 { neg_mem := λ S x hx, neg_one_smul R x ▸ S.smul_mem hx _,
   .. subalgebra.subsemiring_class }
 
-theorem neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
+protected theorem neg_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) : -x ∈ S :=
-neg_one_smul R x ▸ S.smul_mem hx _
-
-theorem sub_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
+neg_mem hx
+protected theorem sub_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x - y ∈ S :=
-by simpa only [sub_eq_add_neg] using S.add_mem hx (S.neg_mem hy)
-
-theorem nsmul_mem {x : A} (hx : x ∈ S) (n : ℕ) : n • x ∈ S :=
-S.to_subsemiring.nsmul_mem hx n
+sub_mem hx hy
 
-theorem zsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
-  [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) : ∀ (n : ℤ), n • x ∈ S
-| (n : ℕ) := by { rw [coe_nat_zsmul], exact S.nsmul_mem hx n }
-| -[1+ n] := by { rw [zsmul_neg_succ_of_nat], exact S.neg_mem (S.nsmul_mem hx _) }
-
-theorem coe_nat_mem (n : ℕ) : (n : A) ∈ S :=
-S.to_subsemiring.coe_nat_mem n
-
-theorem coe_int_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
+protected theorem zsmul_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
+  [algebra R A] (S : subalgebra R A) {x : A} (hx : x ∈ S) (n : ℤ) : n • x ∈ S :=
+zsmul_mem hx n
+protected theorem coe_int_mem {R : Type u} {A : Type v} [comm_ring R] [ring A]
   [algebra R A] (S : subalgebra R A) (n : ℤ) : (n : A) ∈ S :=
-int.cases_on n (λ i, S.coe_nat_mem i) (λ i, S.neg_mem $ S.coe_nat_mem $ i + 1)
-
-theorem list_prod_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S :=
-S.to_subsemiring.list_prod_mem h
-
-theorem list_sum_mem {L : list A} (h : ∀ x ∈ L, x ∈ S) : L.sum ∈ S :=
-S.to_subsemiring.list_sum_mem h
-
-theorem multiset_prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
-  [algebra R A] (S : subalgebra R A) {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.prod ∈ S :=
-S.to_subsemiring.multiset_prod_mem m h
-
-theorem multiset_sum_mem {m : multiset A} (h : ∀ x ∈ m, x ∈ S) : m.sum ∈ S :=
-S.to_subsemiring.multiset_sum_mem m h
-
-theorem prod_mem {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
-  [algebra R A] (S : subalgebra R A) {ι : Type w} {t : finset ι} {f : ι → A}
-  (h : ∀ x ∈ t, f x ∈ S) : ∏ x in t, f x ∈ S :=
-S.to_subsemiring.prod_mem h
-
-theorem sum_mem {ι : Type w} {t : finset ι} {f : ι → A}
-  (h : ∀ x ∈ t, f x ∈ S) : ∑ x in t, f x ∈ S :=
-S.to_subsemiring.sum_mem h
+coe_int_mem S n
 
 /-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/
 def to_add_submonoid {R : Type u} {A : Type v} [comm_semiring R] [semiring A] [algebra R A]
@@ -278,22 +255,19 @@ instance : algebra R S := S.algebra'
 
 end
 
-instance nontrivial [nontrivial A] : nontrivial S :=
-S.to_subsemiring.nontrivial
-
 instance no_zero_smul_divisors_bot [no_zero_smul_divisors R A] : no_zero_smul_divisors R S :=
 ⟨λ c x h,
   have c = 0 ∨ (x : A) = 0,
   from eq_zero_or_eq_zero_of_smul_eq_zero (congr_arg coe h),
   this.imp_right (@subtype.ext_iff _ _ x 0).mpr⟩
 
-@[simp, norm_cast] lemma coe_add (x y : S) : (↑(x + y) : A) = ↑x + ↑y := rfl
-@[simp, norm_cast] lemma coe_mul (x y : S) : (↑(x * y) : A) = ↑x * ↑y := rfl
-@[simp, norm_cast] lemma coe_zero : ((0 : S) : A) = 0 := rfl
-@[simp, norm_cast] lemma coe_one : ((1 : S) : A) = 1 := rfl
-@[simp, norm_cast] lemma coe_neg {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
+protected lemma coe_add (x y : S) : (↑(x + y) : A) = ↑x + ↑y := rfl
+protected lemma coe_mul (x y : S) : (↑(x * y) : A) = ↑x * ↑y := rfl
+protected lemma coe_zero : ((0 : S) : A) = 0 := rfl
+protected lemma coe_one : ((1 : S) : A) = 1 := rfl
+protected lemma coe_neg {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
   {S : subalgebra R A} (x : S) : (↑(-x) : A) = -↑x := rfl
-@[simp, norm_cast] lemma coe_sub {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
+protected lemma coe_sub {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
   {S : subalgebra R A} (x y : S) : (↑(x - y) : A) = ↑x - ↑y := rfl
 @[simp, norm_cast] lemma coe_smul [semiring R'] [has_scalar R' R] [module R' A]
   [is_scalar_tower R' R A] (r : R') (x : S) : (↑(r • x) : A) = r • ↑x := rfl
@@ -301,17 +275,9 @@ instance no_zero_smul_divisors_bot [no_zero_smul_divisors R A] : no_zero_smul_di
   [is_scalar_tower R' R A] (r : R') :
   ↑(algebra_map R' S r) = algebra_map R' A r := rfl
 
-@[simp, norm_cast] lemma coe_pow (x : S) (n : ℕ) : (↑(x^n) : A) = (↑x)^n :=
-begin
-  induction n with n ih,
-  { simp, },
-  { simp [pow_succ, ih], },
-end
-
-@[simp, norm_cast] lemma coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 :=
-(subtype.ext_iff.symm : (x : A) = (0 : S) ↔ x = 0)
-@[simp, norm_cast] lemma coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 :=
-(subtype.ext_iff.symm : (x : A) = (1 : S) ↔ x = 1)
+protected lemma coe_pow (x : S) (n : ℕ) : (↑(x^n) : A) = (↑x)^n := submonoid_class.coe_pow x n
+protected lemma coe_eq_zero {x : S} : (x : A) = 0 ↔ x = 0 := add_submonoid_class.coe_eq_zero
+protected lemma coe_eq_one {x : S} : (x : A) = 1 ↔ x = 1 := submonoid_class.coe_eq_one
 
 -- todo: standardize on the names these morphisms
 -- compare with submodule.subtype
@@ -731,7 +697,7 @@ alg_equiv.of_alg_hom (subalgebra.val ⊤) to_top rfl $ alg_hom.ext $ λ _, subty
 
 -- TODO[gh-6025]: make this an instance once safe to do so
 lemma subsingleton_of_subsingleton [subsingleton A] : subsingleton (subalgebra R A) :=
-⟨λ B C, ext (λ x, by { simp only [subsingleton.elim x 0, zero_mem] })⟩
+⟨λ B C, ext (λ x, by { simp only [subsingleton.elim x 0, zero_mem B, zero_mem C] })⟩
 
 /--
 For performance reasons this is not an instance. If you need this instance, add
@@ -1094,7 +1060,7 @@ variables {R : Type*} [semiring R]
 
 /-- A subsemiring is a `ℕ`-subalgebra. -/
 def subalgebra_of_subsemiring (S : subsemiring R) : subalgebra ℕ R :=
-{ algebra_map_mem' := λ i, S.coe_nat_mem i,
+{ algebra_map_mem' := λ i, coe_nat_mem S i,
   .. S }
 
 @[simp] lemma mem_subalgebra_of_subsemiring {x : R} {S : subsemiring R} :
diff --git a/src/algebra/algebra/subalgebra/pointwise.lean b/src/algebra/algebra/subalgebra/pointwise.lean
index b61c0cc3778df..70ffd9895815a 100644
--- a/src/algebra/algebra/subalgebra/pointwise.lean
+++ b/src/algebra/algebra/subalgebra/pointwise.lean
@@ -25,7 +25,8 @@ theorem mul_to_submodule_le (S T : subalgebra R A) :
 begin
   rw submodule.mul_le,
   intros y hy z hz,
-  exact mul_mem _ (algebra.mem_sup_left hy) (algebra.mem_sup_right hz),
+  show y * z ∈ (S ⊔ T),
+  exact mul_mem (algebra.mem_sup_left hy) (algebra.mem_sup_right hz),
 end
 
 /-- As submodules, subalgebras are idempotent. -/
@@ -36,7 +37,7 @@ begin
     rw sup_idem },
   { intros x hx1,
     rw ← mul_one x,
-    exact submodule.mul_mem_mul hx1 (one_mem S) }
+    exact submodule.mul_mem_mul hx1 (show (1 : A) ∈ S, from one_mem S) }
 end
 
 /-- When `A` is commutative, `subalgebra.mul_to_submodule_le` is strict. -/
@@ -50,11 +51,11 @@ begin
     (λ x y hx hy, _),
   { cases hx with hxS hxT,
     { rw ← mul_one x,
-      exact submodule.mul_mem_mul hxS (one_mem T) },
+      exact submodule.mul_mem_mul hxS (show (1 : A) ∈ T, from one_mem T) },
     { rw ← one_mul x,
-      exact submodule.mul_mem_mul (one_mem S) hxT } },
+      exact submodule.mul_mem_mul (show (1 : A) ∈ S, from one_mem S) hxT } },
   { rw ← one_mul (algebra_map _ _ _),
-    exact submodule.mul_mem_mul (one_mem S) (algebra_map_mem _ _) },
+    exact submodule.mul_mem_mul (show (1 : A) ∈ S, from one_mem S) (algebra_map_mem _ _) },
   have := submodule.mul_mem_mul hx hy,
   rwa [mul_assoc, mul_comm _ T.to_submodule, ←mul_assoc _ _ S.to_submodule, mul_self,
     mul_comm T.to_submodule, ←mul_assoc, mul_self] at this,
diff --git a/src/algebra/algebra/tower.lean b/src/algebra/algebra/tower.lean
index a56cac507cb5b..fdbf486098571 100644
--- a/src/algebra/algebra/tower.lean
+++ b/src/algebra/algebra/tower.lean
@@ -309,7 +309,7 @@ theorem smul_mem_span_smul_of_mem {s : set S} {t : set A} {k : S} (hks : k ∈ s
   {x : A} (hx : x ∈ t) : k • x ∈ span R (s • t) :=
 span_induction hks (λ c hc, subset_span $ set.mem_smul.2 ⟨c, x, hc, hx, rfl⟩)
   (by { rw zero_smul, exact zero_mem _ })
-  (λ c₁ c₂ ih₁ ih₂, by { rw add_smul, exact add_mem _ ih₁ ih₂ })
+  (λ c₁ c₂ ih₁ ih₂, by { rw add_smul, exact add_mem ih₁ ih₂ })
   (λ b c hc, by { rw is_scalar_tower.smul_assoc, exact smul_mem _ _ hc })
 
 variables [smul_comm_class R S A]
@@ -319,7 +319,7 @@ theorem smul_mem_span_smul {s : set S} (hs : span R s = ⊤) {t : set A} {k : S}
   k • x ∈ span R (s • t) :=
 span_induction hx (λ x hx, smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hx)
   (by { rw smul_zero, exact zero_mem _ })
-  (λ x y ihx ihy, by { rw smul_add, exact add_mem _ ihx ihy })
+  (λ x y ihx ihy, by { rw smul_add, exact add_mem ihx ihy })
   (λ c x hx, smul_comm c k x ▸ smul_mem _ _ hx)
 
 theorem smul_mem_span_smul' {s : set S} (hs : span R s = ⊤) {t : set A} {k : S}
@@ -328,7 +328,7 @@ theorem smul_mem_span_smul' {s : set S} (hs : span R s = ⊤) {t : set A} {k : S
 span_induction hx (λ x hx, let ⟨p, q, hp, hq, hpq⟩ := set.mem_smul.1 hx in
     by { rw [← hpq, smul_smul], exact smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hq })
   (by { rw smul_zero, exact zero_mem _ })
-  (λ x y ihx ihy, by { rw smul_add, exact add_mem _ ihx ihy })
+  (λ x y ihx ihy, by { rw smul_add, exact add_mem ihx ihy })
   (λ c x hx, smul_comm c k x ▸ smul_mem _ _ hx)
 
 theorem span_smul {s : set S} (hs : span R s = ⊤) (t : set A) :
@@ -337,7 +337,7 @@ le_antisymm (span_le.2 $ λ x hx, let ⟨p, q, hps, hqt, hpqx⟩ := set.mem_smul
   hpqx ▸ (span S t).smul_mem p (subset_span hqt)) $
 λ p hp, span_induction hp (λ x hx, one_smul S x ▸ smul_mem_span_smul hs (subset_span hx))
   (zero_mem _)
-  (λ _ _, add_mem _)
+  (λ _ _, add_mem)
   (λ k x hx, smul_mem_span_smul' hs hx)
 
 end module
diff --git a/src/algebra/direct_sum/internal.lean b/src/algebra/direct_sum/internal.lean
index 1a9ec0132bfdc..b02cc3edd749a 100644
--- a/src/algebra/direct_sum/internal.lean
+++ b/src/algebra/direct_sum/internal.lean
@@ -97,7 +97,7 @@ lemma direct_sum.coe_mul_apply_add_submonoid [add_monoid ι] [semiring R]
       r ij.1 * r' ij.2 :=
 begin
   rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
-    add_submonoid.coe_finset_sum],
+    add_submonoid_class.coe_finset_sum],
   simp_rw [direct_sum.coe_of_add_submonoid_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
 end
 
@@ -139,7 +139,7 @@ lemma direct_sum.coe_mul_apply_add_subgroup [add_monoid ι] [ring R]
       r ij.1 * r' ij.2 :=
 begin
   rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
-    add_subgroup.coe_finset_sum],
+    add_submonoid_class.coe_finset_sum],
   simp_rw [direct_sum.coe_of_add_subgroup_apply, ←finset.sum_filter, set_like.coe_ghas_mul],
 end
 
diff --git a/src/algebra/lie/cartan_subalgebra.lean b/src/algebra/lie/cartan_subalgebra.lean
index aa4e7b7214cff..0c1204888eb1a 100644
--- a/src/algebra/lie/cartan_subalgebra.lean
+++ b/src/algebra/lie/cartan_subalgebra.lean
@@ -43,7 +43,7 @@ def normalizer : lie_subalgebra R L :=
 lemma mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ (y : L), (y ∈ H) → ⁅x, y⁆ ∈ H := iff.rfl
 
 lemma mem_normalizer_iff' (x : L) : x ∈ H.normalizer ↔ ∀ (y : L), (y ∈ H) → ⁅y, x⁆ ∈ H :=
-forall₂_congr $ λ y hy, by rw [← lie_skew, H.neg_mem_iff]
+forall₂_congr $ λ y hy, by rw [← lie_skew, neg_mem_iff]
 
 lemma le_normalizer : H ≤ H.normalizer :=
 λ x hx, show ∀ (y : L), y ∈ H → ⁅x,y⁆ ∈ H, from λ y, H.lie_mem hx
diff --git a/src/algebra/lie/subalgebra.lean b/src/algebra/lie/subalgebra.lean
index 04847fe59df12..5dfce2b1c2894 100644
--- a/src/algebra/lie/subalgebra.lean
+++ b/src/algebra/lie/subalgebra.lean
@@ -52,8 +52,6 @@ instance : has_coe (lie_subalgebra R L) (submodule R L) := ⟨lie_subalgebra.to_
 
 namespace lie_subalgebra
 
-open neg_mem_class
-
 instance : set_like (lie_subalgebra R L) L :=
 { coe := λ L', L',
   coe_injective' := λ L' L'' h, by { rcases L' with ⟨⟨⟩⟩, rcases L'' with ⟨⟨⟩⟩, congr' } }
@@ -97,18 +95,12 @@ instance (L' : lie_subalgebra R L) : lie_algebra R L' :=
 
 variables {R L} (L' : lie_subalgebra R L)
 
-@[simp] lemma zero_mem : (0 : L) ∈ L' := (L' : submodule R L).zero_mem
+@[simp] protected lemma zero_mem : (0 : L) ∈ L' := zero_mem L'
+protected lemma add_mem {x y : L} : x ∈ L' → y ∈ L' → (x + y : L) ∈ L' := add_mem
+protected lemma sub_mem {x y : L} : x ∈ L' → y ∈ L' → (x - y : L) ∈ L' := sub_mem
 
 lemma smul_mem (t : R) {x : L} (h : x ∈ L') : t • x ∈ L' := (L' : submodule R L).smul_mem t h
 
-lemma add_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (x + y : L) ∈ L' :=
-(L' : submodule R L).add_mem hx hy
-
-lemma sub_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (x - y : L) ∈ L' :=
-(L' : submodule R L).sub_mem hx hy
-
-@[simp] lemma neg_mem_iff {x : L} : -x ∈ L' ↔ x ∈ L' := L'.to_submodule.neg_mem_iff
-
 lemma lie_mem {x y : L} (hx : x ∈ L') (hy : y ∈ L') : (⁅x, y⁆ : L) ∈ L' := L'.lie_mem' hx hy
 
 @[simp] lemma mem_carrier {x : L} : x ∈ L'.carrier ↔ x ∈ (L' : set L) := iff.rfl
diff --git a/src/algebra/lie/submodule.lean b/src/algebra/lie/submodule.lean
index 4553905a4376c..c4794edc3829d 100644
--- a/src/algebra/lie/submodule.lean
+++ b/src/algebra/lie/submodule.lean
@@ -49,8 +49,6 @@ namespace lie_submodule
 
 variables {R L M} (N N' : lie_submodule R L M)
 
-open neg_mem_class
-
 instance : set_like (lie_submodule R L M) M :=
 { coe := carrier,
   coe_injective' := λ N O h, by cases N; cases O; congr' }
@@ -85,7 +83,7 @@ iff.rfl
 
 lemma mem_coe {x : M} : x ∈ (N : set M) ↔ x ∈ N := iff.rfl
 
-@[simp] lemma zero_mem : (0 : M) ∈ N := (N : submodule R M).zero_mem
+@[simp] protected lemma zero_mem : (0 : M) ∈ N := zero_mem N
 
 @[simp] lemma mk_eq_zero {x} (h : x ∈ N) : (⟨x, h⟩ : N) = 0 ↔ x = 0 := subtype.ext_iff_val
 
diff --git a/src/algebra/module/submodule.lean b/src/algebra/module/submodule.lean
index b21d63b6b6227..cff1388b1ad80 100644
--- a/src/algebra/module/submodule.lean
+++ b/src/algebra/module/submodule.lean
@@ -139,27 +139,26 @@ variables {r : R} {x y : M}
 variables (p)
 @[simp] lemma mem_carrier : x ∈ p.carrier ↔ x ∈ (p : set M) := iff.rfl
 
-@[simp] lemma zero_mem : (0 : M) ∈ p := p.zero_mem'
-
-lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := p.add_mem' h₁ h₂
+@[simp] protected lemma zero_mem : (0 : M) ∈ p := zero_mem _
+protected lemma add_mem (h₁ : x ∈ p) (h₂ : y ∈ p) : x + y ∈ p := add_mem h₁ h₂
 
 lemma smul_mem (r : R) (h : x ∈ p) : r • x ∈ p := p.smul_mem' r h
 lemma smul_of_tower_mem [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M]
   (r : S) (h : x ∈ p) : r • x ∈ p :=
 p.to_sub_mul_action.smul_of_tower_mem r h
 
-lemma sum_mem {t : finset ι} {f : ι → M} : (∀c∈t, f c ∈ p) → (∑ i in t, f i) ∈ p :=
-p.to_add_submonoid.sum_mem
+protected lemma sum_mem {t : finset ι} {f : ι → M} : (∀c∈t, f c ∈ p) → (∑ i in t, f i) ∈ p :=
+sum_mem
 
 lemma sum_smul_mem {t : finset ι} {f : ι → M} (r : ι → R)
     (hyp : ∀ c ∈ t, f c ∈ p) : (∑ i in t, r i • f i) ∈ p :=
-submodule.sum_mem _ (λ i hi, submodule.smul_mem  _ _ (hyp i hi))
+sum_mem (λ i hi, smul_mem _ _ (hyp i hi))
 
 @[simp] lemma smul_mem_iff' [group G] [mul_action G M] [has_scalar G R] [is_scalar_tower G R M]
   (g : G) : g • x ∈ p ↔ x ∈ p :=
 p.to_sub_mul_action.smul_mem_iff' g
 
-instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem _ x.2 y.2⟩⟩
+instance : has_add p := ⟨λx y, ⟨x.1 + y.1, add_mem x.2 y.2⟩⟩
 instance : has_zero p := ⟨⟨0, zero_mem _⟩⟩
 instance : inhabited p := ⟨0⟩
 instance [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] :
@@ -291,7 +290,7 @@ instance [module R M] : add_subgroup_class (submodule R M) M :=
 { neg_mem := λ p x, p.to_sub_mul_action.neg_mem,
   .. submodule.add_submonoid_class }
 
-lemma neg_mem (hx : x ∈ p) : -x ∈ p := neg_mem_class.neg_mem hx
+protected lemma neg_mem (hx : x ∈ p) : -x ∈ p := neg_mem hx
 
 /-- Reinterpret a submodule as an additive subgroup. -/
 def to_add_subgroup : add_subgroup M :=
@@ -319,13 +318,12 @@ to_add_subgroup_strict_mono.monotone
 
 omit module_M
 
-lemma sub_mem : x ∈ p → y ∈ p → x - y ∈ p := p.to_add_subgroup.sub_mem
-
-@[simp] lemma neg_mem_iff : -x ∈ p ↔ x ∈ p := p.to_add_subgroup.neg_mem_iff
-
-lemma add_mem_iff_left : y ∈ p → (x + y ∈ p ↔ x ∈ p) := p.to_add_subgroup.add_mem_cancel_right
-
-lemma add_mem_iff_right : x ∈ p → (x + y ∈ p ↔ y ∈ p) := p.to_add_subgroup.add_mem_cancel_left
+protected lemma sub_mem : x ∈ p → y ∈ p → x - y ∈ p := sub_mem
+protected lemma neg_mem_iff : -x ∈ p ↔ x ∈ p := neg_mem_iff
+protected lemma add_mem_iff_left : y ∈ p → (x + y ∈ p ↔ x ∈ p) := add_mem_cancel_right
+protected lemma add_mem_iff_right : x ∈ p → (x + y ∈ p ↔ y ∈ p) := add_mem_cancel_left
+protected lemma coe_neg (x : p) : ((-x : p) : M) = -x := add_subgroup_class.coe_neg _
+protected lemma coe_sub (x y : p) : (↑(x - y) : M) = ↑x - ↑y := add_subgroup_class.coe_sub _ _
 
 lemma sub_mem_iff_left (hy : y ∈ p) : (x - y) ∈ p ↔ x ∈ p :=
 by rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
@@ -333,15 +331,9 @@ by rw [sub_eq_add_neg, p.add_mem_iff_left (p.neg_mem hy)]
 lemma sub_mem_iff_right (hx : x ∈ p) : (x - y) ∈ p ↔ y ∈ p :=
 by rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]
 
-instance : has_neg p := ⟨λx, ⟨-x.1, neg_mem _ x.2⟩⟩
-
-@[simp, norm_cast] lemma coe_neg (x : p) : ((-x : p) : M) = -x := rfl
-
 instance : add_comm_group p :=
 { add := (+), zero := 0, neg := has_neg.neg, ..p.to_add_subgroup.to_add_comm_group }
 
-@[simp, norm_cast] lemma coe_sub (x y : p) : (↑(x - y) : M) = ↑x - ↑y := rfl
-
 end add_comm_group
 
 section is_domain
diff --git a/src/algebra/module/submodule_lattice.lean b/src/algebra/module/submodule_lattice.lean
index 7d96a3ac74fb6..2a424b500e5d0 100644
--- a/src/algebra/module/submodule_lattice.lean
+++ b/src/algebra/module/submodule_lattice.lean
@@ -57,7 +57,7 @@ instance unique_bot : unique (⊥ : submodule R M) :=
 
 instance : order_bot (submodule R M) :=
 { bot := ⊥,
-  bot_le := λ p x, by simp {contextual := tt} }
+  bot_le := λ p x, by simp [zero_mem] {contextual := tt} }
 
 protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
 ⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
@@ -135,7 +135,7 @@ This is the module version of `add_submonoid.top_equiv`. -/
 instance : has_Inf (submodule R M) :=
 ⟨λ S,
 { carrier   := ⋂ s ∈ S, (s : set M),
-  zero_mem' := by simp,
+  zero_mem' := by simp [zero_mem],
   add_mem'  := by simp [add_mem] {contextual := tt},
   smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
 
@@ -148,7 +148,7 @@ set.subset_Inter₂
 instance : has_inf (submodule R M) :=
 ⟨λ p q,
 { carrier   := p ∩ q,
-  zero_mem' := by simp,
+  zero_mem' := by simp [zero_mem],
   add_mem'  := by simp [add_mem] {contextual := tt},
   smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
 
@@ -211,7 +211,7 @@ lemma mem_sup_right {S T : submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔
 show T ≤ S ⊔ T, from le_sup_right
 
 lemma add_mem_sup {S T : submodule R M} {s t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T :=
-add_mem _ (mem_sup_left hs) (mem_sup_right ht)
+add_mem (mem_sup_left hs) (mem_sup_right ht)
 
 lemma mem_supr_of_mem {ι : Sort*} {b : M} {p : ι → submodule R M} (i : ι) (h : b ∈ p i) :
   b ∈ (⨆i, p i) :=
@@ -223,12 +223,12 @@ open_locale big_operators
 lemma sum_mem_supr {ι : Type*} [fintype ι] {f : ι → M} {p : ι → submodule R M}
   (h : ∀ i, f i ∈ p i) :
   ∑ i, f i ∈ ⨆ i, p i :=
-sum_mem _ $ λ i hi, mem_supr_of_mem i (h i)
+sum_mem $ λ i hi, mem_supr_of_mem i (h i)
 
 lemma sum_mem_bsupr {ι : Type*} {s : finset ι} {f : ι → M} {p : ι → submodule R M}
   (h : ∀ i ∈ s, f i ∈ p i) :
   ∑ i in s, f i ∈ ⨆ i ∈ s, p i :=
-sum_mem _ $ λ i hi, mem_supr_of_mem i $ mem_supr_of_mem hi (h i hi)
+sum_mem $ λ i hi, mem_supr_of_mem i $ mem_supr_of_mem hi (h i hi)
 
 /-! Note that `submodule.mem_supr` is provided in `linear_algebra/basic.lean`. -/
 
@@ -256,7 +256,7 @@ section nat_submodule
 /-- An additive submonoid is equivalent to a ℕ-submodule. -/
 def add_submonoid.to_nat_submodule : add_submonoid M ≃o submodule ℕ M :=
 { to_fun := λ S,
-  { smul_mem' := λ r s hs, S.nsmul_mem hs _, ..S },
+  { smul_mem' := λ r s hs, show r • s ∈ S, from nsmul_mem hs _, ..S },
   inv_fun := submodule.to_add_submonoid,
   left_inv := λ ⟨S, _, _⟩, rfl,
   right_inv := λ ⟨S, _, _, _⟩, rfl,
diff --git a/src/algebra/star/unitary.lean b/src/algebra/star/unitary.lean
index b0053664e7556..026a343eaafb3 100644
--- a/src/algebra/star/unitary.lean
+++ b/src/algebra/star/unitary.lean
@@ -121,7 +121,7 @@ by simp only [div_eq_mul_inv, coe_inv, submonoid.coe_mul]
 @[norm_cast] lemma coe_zpow (U : unitary R) (z : ℤ) : ↑(U ^ z) = (U ^ z : R) :=
 begin
   induction z,
-  { simp [submonoid.coe_pow], },
+  { simp [submonoid_class.coe_pow], },
   { simp [coe_inv] },
 end
 
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
index b73b00f16da50..f77c7c9b4737a 100644
--- a/src/analysis/convex/basic.lean
+++ b/src/analysis/convex/basic.lean
@@ -1067,7 +1067,7 @@ open submodule
 
 lemma submodule.convex [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] (K : submodule 𝕜 E) :
   convex 𝕜 (↑K : set E) :=
-by { repeat {intro}, refine add_mem _ (smul_mem _ _ _) (smul_mem _ _ _); assumption }
+by { repeat {intro}, refine add_mem (smul_mem _ _ _) (smul_mem _ _ _); assumption }
 
 lemma subspace.convex [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] (K : subspace 𝕜 E) :
   convex 𝕜 (↑K : set E) :=
diff --git a/src/analysis/convex/cone.lean b/src/analysis/convex/cone.lean
index 8ca93e7b304c4..b45d9b5b99da6 100644
--- a/src/analysis/convex/cone.lean
+++ b/src/analysis/convex/cone.lean
@@ -461,11 +461,11 @@ begin
       by simpa only [set.nonempty, upper_bounds, lower_bounds, ball_image_iff] using this,
     refine exists_between_of_forall_le (nonempty.image f _) (nonempty.image f (dense y)) _,
     { rcases (dense (-y)) with ⟨x, hx⟩,
-      rw [← neg_neg x, coe_neg, ← sub_eq_add_neg] at hx,
+      rw [← neg_neg x, add_subgroup_class.coe_neg, ← sub_eq_add_neg] at hx,
       exact ⟨_, hx⟩ },
     rintros a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩,
     have := s.add_mem hxp hxn,
-    rw [add_assoc, add_sub_cancel'_right, ← sub_eq_add_neg, ← coe_sub] at this,
+    rw [add_assoc, add_sub_cancel'_right, ← sub_eq_add_neg, ← add_subgroup_class.coe_sub] at this,
     replace := nonneg _ this,
     rwa [f.map_sub, sub_nonneg] at this },
   have hy' : y ≠ 0, from λ hy₀, hy (hy₀.symm ▸ zero_mem _),
diff --git a/src/analysis/inner_product_space/l2_space.lean b/src/analysis/inner_product_space/l2_space.lean
index 107df8aeee86f..93269208a2498 100644
--- a/src/analysis/inner_product_space/l2_space.lean
+++ b/src/analysis/inner_product_space/l2_space.lean
@@ -228,7 +228,8 @@ begin
   { rintros x ⟨f, rfl⟩,
     refine mem_closure_of_tendsto (hV.has_sum_linear_isometry f) (eventually_of_forall _),
     intros s,
-    refine sum_mem (supr (λ i, (V i).to_linear_map.range)) _,
+    rw set_like.mem_coe,
+    refine sum_mem _,
     intros i hi,
     refine mem_supr_of_mem i _,
     exact linear_map.mem_range_self _ (f i) },
@@ -379,7 +380,7 @@ begin
   refine mem_closure_of_tendsto (b.has_sum_repr x) (eventually_of_forall _),
   intros s,
   simp only [set_like.mem_coe],
-  refine sum_mem _ _,
+  refine sum_mem _,
   rintros i -,
   refine smul_mem _ _ _,
   exact subset_span ⟨i, rfl⟩
diff --git a/src/data/dfinsupp/basic.lean b/src/data/dfinsupp/basic.lean
index ad0019ad184c5..13a6cfddc1120 100644
--- a/src/data/dfinsupp/basic.lean
+++ b/src/data/dfinsupp/basic.lean
@@ -1161,13 +1161,13 @@ calc ∏ i in (f + g).support, h i ((f + g) i) =
   ... = _ : by rw [f_eq, g_eq]
 
 @[to_additive]
-lemma _root_.submonoid.dfinsupp_prod_mem [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]
-  [comm_monoid γ] (S : submonoid γ)
-  (f : Π₀ i, β i) (g : Π i, β i → γ) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.prod g ∈ S :=
-S.prod_mem $ λ i hi, h _ $ mem_support_iff.1 hi
+lemma _root_.dfinsupp_prod_mem [Π i, has_zero (β i)] [Π i (x : β i), decidable (x ≠ 0)]
+  [comm_monoid γ] {S : Type*} [set_like S γ] [submonoid_class S γ] (s : S)
+  (f : Π₀ i, β i) (g : Π i, β i → γ) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
+prod_mem $ λ i hi, h _ $ mem_support_iff.1 hi
 
 @[simp, to_additive] lemma prod_eq_prod_fintype [fintype ι] [Π i, has_zero (β i)]
-  [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid γ] (v : Π₀ i, β i) {f : Π i, β i → γ}
+  [Π (i : ι) (x : β i), decidable (x ≠ 0)] [comm_monoid γ] (v : Π₀ i, β i) [f : Π i, β i → γ]
   (hf : ∀ i, f i 0 = 1) :
   v.prod f = ∏ i, f i (dfinsupp.equiv_fun_on_fintype v i) :=
 begin
@@ -1244,13 +1244,14 @@ begin
   rw [(not_not.mp h), add_monoid_hom.map_zero],
 end
 
-lemma _root_.add_submonoid.dfinsupp_sum_add_hom_mem [Π i, add_zero_class (β i)] [add_comm_monoid γ]
-  (S : add_submonoid γ) (f : Π₀ i, β i) (g : Π i, β i →+ γ) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
-  dfinsupp.sum_add_hom g f ∈ S :=
+lemma _root_.dfinsupp_sum_add_hom_mem [Π i, add_zero_class (β i)] [add_comm_monoid γ] {S : Type*}
+  [set_like S γ] [add_submonoid_class S γ] (s : S) (f : Π₀ i, β i) (g : Π i, β i →+ γ)
+  (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : dfinsupp.sum_add_hom g f ∈ s :=
 begin
   classical,
   rw dfinsupp.sum_add_hom_apply,
-  convert S.dfinsupp_sum_mem _ _ _,
+  convert dfinsupp_sum_mem _ _ _ _,
+  { apply_instance },
   exact h
 end
 
@@ -1265,7 +1266,7 @@ begin
     intros i y hy,
     exact ⟨dfinsupp.single i ⟨y, hy⟩, dfinsupp.sum_add_hom_single _ _ _⟩, },
   { rintros x ⟨v, rfl⟩,
-    exact add_submonoid.dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr S i : S i ≤ _) (v i).prop) }
+    exact dfinsupp_sum_add_hom_mem _ v _ (λ i _, (le_supr S i : S i ≤ _) (v i).prop) }
 end
 
 /-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
@@ -1282,7 +1283,7 @@ begin
     rw [add_monoid_hom.comp_apply, filter_add_monoid_hom_apply, filter_single_pos _ _ hi],
     exact sum_add_hom_single _ _ _, },
   { rintros x ⟨v, rfl⟩,
-    refine add_submonoid.dfinsupp_sum_add_hom_mem _ _ _ (λ i hi, _),
+    refine dfinsupp_sum_add_hom_mem _ _ _ (λ i hi, _),
     refine add_submonoid.mem_supr_of_mem i _,
     by_cases hp : p i,
     { simp [hp], },
diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
index 45f08db0f8411..47d7ddfd2d2d8 100644
--- a/src/data/finsupp/basic.lean
+++ b/src/data/finsupp/basic.lean
@@ -819,9 +819,9 @@ begin
 end
 
 @[to_additive]
-lemma _root_.submonoid.finsupp_prod_mem (S : submonoid N) (f : α →₀ M) (g : α → M → N)
-  (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.prod g ∈ S :=
-S.prod_mem $ λ i hi, h _ (finsupp.mem_support_iff.mp hi)
+lemma _root_.submonoid_class.finsupp_prod_mem {S : Type*} [set_like S N] [submonoid_class S N]
+  (s : S) (f : α →₀ M) (g : α → M → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ s) : f.prod g ∈ s :=
+prod_mem $ λ i hi, h _ (finsupp.mem_support_iff.mp hi)
 
 @[to_additive]
 lemma prod_congr {f : α →₀ M} {g1 g2 : α → M → N}
diff --git a/src/data/set/pointwise.lean b/src/data/set/pointwise.lean
index 0944af589c088..8e363e561fdf8 100644
--- a/src/data/set/pointwise.lean
+++ b/src/data/set/pointwise.lean
@@ -1283,7 +1283,7 @@ begin
   { exact ⟨0, by simpa using one_mem _⟩ },
   { rintro x y ⟨nx, hx⟩ ⟨ny, hy⟩,
     use nx + ny,
-    convert mul_mem _ hx hy,
+    convert mul_mem hx hy,
     rw [pow_add, smul_mul_assoc, mul_smul, mul_comm, ← smul_mul_assoc, mul_comm] }
 end
 
diff --git a/src/deprecated/subgroup.lean b/src/deprecated/subgroup.lean
index f9db55de6b814..b07d7ac513966 100644
--- a/src/deprecated/subgroup.lean
+++ b/src/deprecated/subgroup.lean
@@ -329,7 +329,8 @@ local attribute [simp] one_mem inv_mem mul_mem is_normal_subgroup.normal
 lemma preimage {f : G → H} (hf : is_group_hom f) {s : set H} (hs : is_subgroup s) :
   is_subgroup (f ⁻¹' s) :=
 by { refine {..};
-     simp [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul, hf.map_one, hf.map_inv, @inv_mem H _ s]
+     simp [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul, hf.map_one, hf.map_inv,
+           inv_mem_class.inv_mem]
      {contextual := tt} }
 
 @[to_additive]
@@ -423,7 +424,7 @@ theorem subset_closure {s : set G} : s ⊆ closure s := λ a, mem_closure
 
 @[to_additive]
 theorem closure_subset {s t : set G} (ht : is_subgroup t) (h : s ⊆ t) : closure s ⊆ t :=
-assume a ha, by induction ha; simp [h _, *, ht.one_mem, ht.mul_mem, inv_mem_iff]
+assume a ha, by induction ha; simp [h _, *, ht.one_mem, ht.mul_mem, is_subgroup.inv_mem_iff]
 
 @[to_additive]
 lemma closure_subset_iff {s t : set G} (ht : is_subgroup t) : closure s ⊆ t ↔ s ⊆ t :=
diff --git a/src/field_theory/abel_ruffini.lean b/src/field_theory/abel_ruffini.lean
index 2824172945578..a127bd921c556 100644
--- a/src/field_theory/abel_ruffini.lean
+++ b/src/field_theory/abel_ruffini.lean
@@ -364,12 +364,12 @@ begin
   revert α,
   apply solvable_by_rad.induction,
   { exact λ α, by { rw minpoly.eq_X_sub_C, exact gal_X_sub_C_is_solvable α } },
-  { exact λ α β, induction2 (add_mem _ (subset_adjoin F _ (set.mem_insert α _))
+  { exact λ α β, induction2 (add_mem (subset_adjoin F _ (set.mem_insert α _))
       (subset_adjoin F _ (set.mem_insert_of_mem α (set.mem_singleton β)))) },
-  { exact λ α, induction1 (neg_mem _ (mem_adjoin_simple_self F α)) },
-  { exact λ α β, induction2 (mul_mem _ (subset_adjoin F _ (set.mem_insert α _))
+  { exact λ α, induction1 (neg_mem (mem_adjoin_simple_self F α)) },
+  { exact λ α β, induction2 (mul_mem (subset_adjoin F _ (set.mem_insert α _))
       (subset_adjoin F _ (set.mem_insert_of_mem α (set.mem_singleton β)))) },
-  { exact λ α, induction1 (inv_mem _ (mem_adjoin_simple_self F α)) },
+  { exact λ α, induction1 (inv_mem (mem_adjoin_simple_self F α)) },
   { exact λ α n, induction3 },
 end
 
diff --git a/src/field_theory/finite/polynomial.lean b/src/field_theory/finite/polynomial.lean
index 6ebeeecfb3f47..8f37c388a6b25 100644
--- a/src/field_theory/finite/polynomial.lean
+++ b/src/field_theory/finite/polynomial.lean
@@ -124,7 +124,7 @@ lemma map_restrict_dom_evalₗ : (restrict_degree σ K (fintype.card K - 1)).map
 begin
   refine top_unique (set_like.le_def.2 $ assume e _, mem_map.2 _),
   refine ⟨∑ n : σ → K, e n • indicator n, _, _⟩,
-  { exact sum_mem _ (assume c _, smul_mem _ _ (indicator_mem_restrict_degree _)) },
+  { exact sum_mem (assume c _, smul_mem _ _ (indicator_mem_restrict_degree _)) },
   { ext n,
     simp only [linear_map.map_sum, @finset.sum_apply (σ → K) (λ_, K) _ _ _ _ _,
       pi.smul_apply, linear_map.map_smul],
diff --git a/src/field_theory/intermediate_field.lean b/src/field_theory/intermediate_field.lean
index 68e97d12e6564..cb35c61de6725 100644
--- a/src/field_theory/intermediate_field.lean
+++ b/src/field_theory/intermediate_field.lean
@@ -90,39 +90,6 @@ set_like.ext h
 @[simp] lemma mem_to_subfield (s : intermediate_field K L) (x : L) :
   x ∈ s.to_subfield ↔ x ∈ s := iff.rfl
 
-/-- An intermediate field contains the image of the smaller field. -/
-theorem algebra_map_mem (x : K) : algebra_map K L x ∈ S :=
-S.algebra_map_mem' x
-
-/-- An intermediate field contains the ring's 1. -/
-theorem one_mem : (1 : L) ∈ S := S.one_mem'
-
-/-- An intermediate field contains the ring's 0. -/
-theorem zero_mem : (0 : L) ∈ S := S.zero_mem'
-
-/-- An intermediate field is closed under multiplication. -/
-theorem mul_mem : ∀ {x y : L}, x ∈ S → y ∈ S → x * y ∈ S := S.mul_mem'
-
-/-- An intermediate field is closed under scalar multiplication. -/
-theorem smul_mem {y : L} : y ∈ S → ∀ {x : K}, x • y ∈ S := S.to_subalgebra.smul_mem
-
-/-- An intermediate field is closed under addition. -/
-theorem add_mem : ∀ {x y : L}, x ∈ S → y ∈ S → x + y ∈ S := S.add_mem'
-
-/-- An intermediate field is closed under subtraction -/
-theorem sub_mem {x y : L} (hx : x ∈ S) (hy : y ∈ S) : x - y ∈ S :=
-S.to_subfield.sub_mem hx hy
-
-/-- An intermediate field is closed under negation. -/
-theorem neg_mem : ∀ {x : L}, x ∈ S → -x ∈ S := S.neg_mem'
-
-/-- An intermediate field is closed under inverses. -/
-theorem inv_mem : ∀ {x : L}, x ∈ S → x⁻¹ ∈ S := S.inv_mem'
-
-/-- An intermediate field is closed under division. -/
-theorem div_mem {x y : L} (hx : x ∈ S) (hy : y ∈ S) : x / y ∈ S :=
-S.to_subfield.div_mem hx hy
-
 /-- Copy of an intermediate field with a new `carrier` equal to the old one. Useful to fix
 definitional equalities. -/
 protected def copy (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
@@ -141,46 +108,71 @@ protected def copy (S : intermediate_field K L) (s : set L) (hs : s = ↑S) :
 lemma copy_eq (S : intermediate_field K L) (s : set L) (hs : s = ↑S) : S.copy s hs = S :=
 set_like.coe_injective hs
 
-/-- Product of a list of elements in an intermediate_field is in the intermediate_field. -/
-lemma list_prod_mem {l : list L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S :=
-S.to_subfield.list_prod_mem
+section inherited_lemmas
 
-/-- Sum of a list of elements in an intermediate field is in the intermediate_field. -/
-lemma list_sum_mem {l : list L} : (∀ x ∈ l, x ∈ S) → l.sum ∈ S :=
-S.to_subfield.list_sum_mem
+/-! ### Lemmas inherited from more general structures
 
-/-- Product of a multiset of elements in an intermediate field is in the intermediate_field. -/
-lemma multiset_prod_mem (m : multiset L) :
-  (∀ a ∈ m, a ∈ S) → m.prod ∈ S :=
-S.to_subfield.multiset_prod_mem m
+The declarations in this section derive from the fact that an `intermediate_field` is also a
+subalgebra or subfield. Their use should be replaceable with the corresponding lemma from a
+subobject class.
+-/
 
+/-- An intermediate field contains the image of the smaller field. -/
+theorem algebra_map_mem (x : K) : algebra_map K L x ∈ S :=
+S.algebra_map_mem' x
+
+/-- An intermediate field is closed under scalar multiplication. -/
+theorem smul_mem {y : L} : y ∈ S → ∀ {x : K}, x • y ∈ S := S.to_subalgebra.smul_mem
+
+/-- An intermediate field contains the ring's 1. -/
+protected theorem one_mem : (1 : L) ∈ S := one_mem S
+/-- An intermediate field contains the ring's 0. -/
+protected theorem zero_mem : (0 : L) ∈ S := zero_mem S
+/-- An intermediate field is closed under multiplication. -/
+protected theorem mul_mem {x y : L} : x ∈ S → y ∈ S → x * y ∈ S := mul_mem
+/-- An intermediate field is closed under addition. -/
+protected theorem add_mem {x y : L} : x ∈ S → y ∈ S → x + y ∈ S := add_mem
+/-- An intermediate field is closed under subtraction -/
+protected theorem sub_mem {x y : L} : x ∈ S → y ∈ S → x - y ∈ S := sub_mem
+/-- An intermediate field is closed under negation. -/
+protected theorem neg_mem {x : L} : x ∈ S → -x ∈ S := neg_mem
+/-- An intermediate field is closed under inverses. -/
+protected theorem inv_mem {x : L} : x ∈ S → x⁻¹ ∈ S := inv_mem
+/-- An intermediate field is closed under division. -/
+protected theorem div_mem {x y : L} : x ∈ S → y ∈ S → x / y ∈ S := div_mem
+
+/-- Product of a list of elements in an intermediate_field is in the intermediate_field. -/
+protected lemma list_prod_mem {l : list L} : (∀ x ∈ l, x ∈ S) → l.prod ∈ S := list_prod_mem
+/-- Sum of a list of elements in an intermediate field is in the intermediate_field. -/
+protected lemma list_sum_mem {l : list L} : (∀ x ∈ l, x ∈ S) → l.sum ∈ S := list_sum_mem
+/-- Product of a multiset of elements in an intermediate field is in the intermediate_field. -/
+protected lemma multiset_prod_mem (m : multiset L) : (∀ a ∈ m, a ∈ S) → m.prod ∈ S :=
+multiset_prod_mem m
 /-- Sum of a multiset of elements in a `intermediate_field` is in the `intermediate_field`. -/
-lemma multiset_sum_mem (m : multiset L) :
-  (∀ a ∈ m, a ∈ S) → m.sum ∈ S :=
-S.to_subfield.multiset_sum_mem m
+protected lemma multiset_sum_mem (m : multiset L) : (∀ a ∈ m, a ∈ S) → m.sum ∈ S :=
+multiset_sum_mem m
 
 /-- Product of elements of an intermediate field indexed by a `finset` is in the intermediate_field.
 -/
-lemma prod_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
-  ∏ i in t, f i ∈ S :=
-S.to_subfield.prod_mem h
-
+protected lemma prod_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
+  ∏ i in t, f i ∈ S := prod_mem h
 /-- Sum of elements in a `intermediate_field` indexed by a `finset` is in the `intermediate_field`.
 -/
-lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
-  ∑ i in t, f i ∈ S :=
-S.to_subfield.sum_mem h
-
-lemma pow_mem {x : L} (hx : x ∈ S) : ∀ (n : ℤ), x^n ∈ S
-| (n : ℕ) := by { rw zpow_coe_nat, exact S.to_subfield.pow_mem hx _, }
-| -[1+ n] := by { rw [zpow_neg_succ_of_nat],
-    exact S.to_subfield.inv_mem (S.to_subfield.pow_mem hx _) }
-
-lemma zsmul_mem {x : L} (hx : x ∈ S) (n : ℤ) :
-  n • x ∈ S := S.to_subfield.zsmul_mem hx n
-
-lemma coe_int_mem (n : ℤ) : (n : L) ∈ S :=
-by simp only [← zsmul_one, zsmul_mem, one_mem]
+protected lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → L} (h : ∀ c ∈ t, f c ∈ S) :
+  ∑ i in t, f i ∈ S := sum_mem h
+protected lemma pow_mem {x : L} (hx : x ∈ S) (n : ℤ) : x^n ∈ S := zpow_mem hx n
+protected lemma zsmul_mem {x : L} (hx : x ∈ S) (n : ℤ) : n • x ∈ S := zsmul_mem hx n
+protected lemma coe_int_mem (n : ℤ) : (n : L) ∈ S := coe_int_mem S n
+
+protected lemma coe_add (x y : S) : (↑(x + y) : L) = ↑x + ↑y := rfl
+protected lemma coe_neg (x : S) : (↑(-x) : L) = -↑x := rfl
+protected lemma coe_mul (x y : S) : (↑(x * y) : L) = ↑x * ↑y := rfl
+protected lemma coe_inv (x : S) : (↑(x⁻¹) : L) = (↑x)⁻¹ := rfl
+protected lemma coe_zero : ((0 : S) : L) = 0 := rfl
+protected lemma coe_one : ((1 : S) : L) = 1 := rfl
+protected lemma coe_pow (x : S) (n : ℕ) : (↑(x ^ n) : L) = ↑x ^ n := submonoid_class.coe_pow x n
+
+end inherited_lemmas
 
 end intermediate_field
 
@@ -215,26 +207,13 @@ namespace intermediate_field
 instance to_field : field S :=
 S.to_subfield.to_field
 
-@[simp, norm_cast] lemma coe_add (x y : S) : (↑(x + y) : L) = ↑x + ↑y := rfl
-@[simp, norm_cast] lemma coe_neg (x : S) : (↑(-x) : L) = -↑x := rfl
-@[simp, norm_cast] lemma coe_mul (x y : S) : (↑(x * y) : L) = ↑x * ↑y := rfl
-@[simp, norm_cast] lemma coe_inv (x : S) : (↑(x⁻¹) : L) = (↑x)⁻¹ := rfl
-@[simp, norm_cast] lemma coe_zero : ((0 : S) : L) = 0 := rfl
-@[simp, norm_cast] lemma coe_one : ((1 : S) : L) = 1 := rfl
-@[simp, norm_cast] lemma coe_pow (x : S) (n : ℕ) : (↑(x ^ n) : L) = ↑x ^ n :=
-begin
-  induction n with n ih,
-  { simp },
-  { simp [pow_succ, ih] }
-end
-
 @[simp, norm_cast]
 lemma coe_sum {ι : Type*} [fintype ι] (f : ι → S) : (↑∑ i, f i : L) = ∑ i, (f i : L) :=
 begin
   classical,
   induction finset.univ using finset.induction_on with i s hi H,
   { simp },
-  { rw [finset.sum_insert hi, coe_add, H, finset.sum_insert hi] }
+  { rw [finset.sum_insert hi, add_submonoid_class.coe_add, H, finset.sum_insert hi] }
 end
 
 @[simp, norm_cast]
@@ -243,7 +222,7 @@ begin
   classical,
   induction finset.univ using finset.induction_on with i s hi H,
   { simp },
-  { rw [finset.prod_insert hi, coe_mul, H, finset.prod_insert hi] }
+  { rw [finset.prod_insert hi, submonoid_class.coe_mul, H, finset.prod_insert hi] }
 end
 
 /-! `intermediate_field`s inherit structure from their `subalgebra` coercions. -/
@@ -320,8 +299,9 @@ lemma aeval_coe {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
   [is_scalar_tower R K L] (x : S) (P : R[X]) : aeval (x : L) P = aeval x P :=
 begin
   refine polynomial.induction_on' P (λ f g hf hg, _) (λ n r, _),
-  { rw [aeval_add, aeval_add, coe_add, hf, hg] },
-  { simp only [coe_mul, aeval_monomial, coe_pow, mul_eq_mul_right_iff],
+  { rw [aeval_add, aeval_add, add_submonoid_class.coe_add, hf, hg] },
+  { simp only [submonoid_class.coe_mul, aeval_monomial, submonoid_class.coe_pow,
+               mul_eq_mul_right_iff],
     left, refl }
 end
 
@@ -336,7 +316,7 @@ begin
       ← is_scalar_tower.algebra_map_eq, ← eval₂_eq_eval_map] },
   { obtain ⟨P, hPmo, hProot⟩ := h,
     refine ⟨P, hPmo, _⟩,
-    rw [← aeval_def, aeval_coe, aeval_def, hProot, coe_zero] },
+    rw [← aeval_def, aeval_coe, aeval_def, hProot, add_submonoid_class.coe_zero] },
 end
 
 variables {S}
@@ -371,11 +351,11 @@ def lift1 {F : intermediate_field K L} (E : intermediate_field K F) : intermedia
 def lift2 {F : intermediate_field K L} (E : intermediate_field F L) : intermediate_field K L :=
 { carrier := E.carrier,
   zero_mem' := zero_mem E,
-  add_mem' := λ x y, add_mem E,
-  neg_mem' := λ x, neg_mem E,
+  add_mem' := λ x y (hx : x ∈ E), add_mem hx,
+  neg_mem' := λ x (hx : x ∈ E), neg_mem hx,
   one_mem' := one_mem E,
-  mul_mem' := λ x y, mul_mem E,
-  inv_mem' := λ x, inv_mem E,
+  mul_mem' := λ x y (hx : x ∈ E), mul_mem hx,
+  inv_mem' := λ x (hx : x ∈ E), inv_mem hx,
   algebra_map_mem' := λ x, algebra_map_mem E (algebra_map K F x) }
 
 instance has_lift1 {F : intermediate_field K L} :
diff --git a/src/field_theory/primitive_element.lean b/src/field_theory/primitive_element.lean
index 13ee954b11cbd..a1f7f32c5683f 100644
--- a/src/field_theory/primitive_element.lean
+++ b/src/field_theory/primitive_element.lean
@@ -57,7 +57,7 @@ begin
     exact F⟮α.val⟯.zero_mem },
   { obtain ⟨n, hn⟩ := set.mem_range.mp (hα (units.mk0 x hx)),
     rw (show x = α^n, by { norm_cast, rw [hn, units.coe_mk0] }),
-    exact pow_mem F⟮↑α⟯ (mem_adjoin_simple_self F ↑α) n, },
+    exact zpow_mem (mem_adjoin_simple_self F ↑α) n, },
 end
 
 /-- Primitive element theorem for finite dimensional extension of a finite field. -/
diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index 506c0169d97b6..4fac3f3053e1f 100644
--- a/src/field_theory/subfield.lean
+++ b/src/field_theory/subfield.lean
@@ -181,66 +181,45 @@ namespace subfield
 
 variables (s t : subfield K)
 
-/-- A subfield contains the ring's 1. -/
-theorem one_mem : (1 : K) ∈ s := s.one_mem'
-
-/-- A subfield contains the ring's 0. -/
-theorem zero_mem : (0 : K) ∈ s := s.zero_mem'
+section derived_from_subfield_class
 
+/-- A subfield contains the field's 1. -/
+protected theorem one_mem : (1 : K) ∈ s := one_mem s
+/-- A subfield contains the field's 0. -/
+protected theorem zero_mem : (0 : K) ∈ s := zero_mem s
 /-- A subfield is closed under multiplication. -/
-theorem mul_mem : ∀ {x y : K}, x ∈ s → y ∈ s → x * y ∈ s := s.mul_mem'
-
+protected theorem mul_mem {x y : K} : x ∈ s → y ∈ s → x * y ∈ s := mul_mem
 /-- A subfield is closed under addition. -/
-theorem add_mem : ∀ {x y : K}, x ∈ s → y ∈ s → x + y ∈ s := s.add_mem'
-
+protected theorem add_mem {x y : K} : x ∈ s → y ∈ s → x + y ∈ s := add_mem
 /-- A subfield is closed under negation. -/
-theorem neg_mem : ∀ {x : K}, x ∈ s → -x ∈ s := s.neg_mem'
-
+protected theorem neg_mem {x : K} : x ∈ s → -x ∈ s := neg_mem
 /-- A subfield is closed under subtraction. -/
-theorem sub_mem {x y : K} : x ∈ s → y ∈ s → x - y ∈ s := s.to_subring.sub_mem
-
+protected theorem sub_mem {x y : K} : x ∈ s → y ∈ s → x - y ∈ s := sub_mem
 /-- A subfield is closed under inverses. -/
-theorem inv_mem : ∀ {x : K}, x ∈ s → x⁻¹ ∈ s := s.inv_mem'
-
+protected theorem inv_mem {x : K} : x ∈ s → x⁻¹ ∈ s := inv_mem
 /-- A subfield is closed under division. -/
-theorem div_mem {x y : K} (hx : x ∈ s) (hy : y ∈ s) : x / y ∈ s :=
-by { rw div_eq_mul_inv, exact s.mul_mem hx (s.inv_mem hy) }
-
+protected theorem div_mem {x y : K} : x ∈ s → y ∈ s → x / y ∈ s := div_mem
 /-- Product of a list of elements in a subfield is in the subfield. -/
-lemma list_prod_mem {l : list K} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s :=
-s.to_submonoid.list_prod_mem
-
+protected lemma list_prod_mem {l : list K} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s := list_prod_mem
 /-- Sum of a list of elements in a subfield is in the subfield. -/
-lemma list_sum_mem {l : list K} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s :=
-s.to_add_subgroup.list_sum_mem
-
+protected lemma list_sum_mem {l : list K} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s := list_sum_mem
 /-- Product of a multiset of elements in a subfield is in the subfield. -/
-lemma multiset_prod_mem (m : multiset K) :
-  (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
-s.to_submonoid.multiset_prod_mem m
-
+protected lemma multiset_prod_mem (m : multiset K) : (∀ a ∈ m, a ∈ s) → m.prod ∈ s :=
+multiset_prod_mem m
 /-- Sum of a multiset of elements in a `subfield` is in the `subfield`. -/
-lemma multiset_sum_mem (m : multiset K) :
-  (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
-s.to_add_subgroup.multiset_sum_mem m
-
+protected lemma multiset_sum_mem (m : multiset K) : (∀ a ∈ m, a ∈ s) → m.sum ∈ s :=
+multiset_sum_mem m
 /-- Product of elements of a subfield indexed by a `finset` is in the subfield. -/
-lemma prod_mem {ι : Type*} {t : finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
+protected lemma prod_mem {ι : Type*} {t : finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
   ∏ i in t, f i ∈ s :=
-s.to_submonoid.prod_mem h
-
+prod_mem h
 /-- Sum of elements in a `subfield` indexed by a `finset` is in the `subfield`. -/
-lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
+protected lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → K} (h : ∀ c ∈ t, f c ∈ s) :
   ∑ i in t, f i ∈ s :=
-s.to_add_subgroup.sum_mem h
-
-lemma pow_mem {x : K} (hx : x ∈ s) (n : ℕ) : x^n ∈ s := s.to_submonoid.pow_mem hx n
-
-lemma zsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) :
-  n • x ∈ s := s.to_add_subgroup.zsmul_mem hx n
-
-lemma coe_int_mem (n : ℤ) : (n : K) ∈ s :=
-by simp only [← zsmul_one, zsmul_mem, one_mem]
+sum_mem h
+protected lemma pow_mem {x : K} (hx : x ∈ s) (n : ℕ) : x^n ∈ s := pow_mem hx n
+protected lemma zsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s := zsmul_mem hx n
+protected lemma coe_int_mem (n : ℤ) : (n : K) ∈ s := coe_int_mem s n
 
 lemma zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x^n ∈ s :=
 begin
@@ -276,6 +255,8 @@ subtype.coe_injective.linear_ordered_field coe
 @[simp, norm_cast] lemma coe_zero : ((0 : s) : K) = 0 := rfl
 @[simp, norm_cast] lemma coe_one : ((1 : s) : K) = 1 := rfl
 
+end derived_from_subfield_class
+
 /-- The embedding from a subfield of the field `K` to `K`. -/
 def subtype (s : subfield K) : s →+* K :=
 { to_fun := coe,
diff --git a/src/group_theory/coset.lean b/src/group_theory/coset.lean
index dab8565578a69..3aa01e43342bf 100644
--- a/src/group_theory/coset.lean
+++ b/src/group_theory/coset.lean
@@ -123,12 +123,12 @@ variables [monoid α] (s : submonoid α)
 @[to_additive mem_own_left_add_coset]
 lemma mem_own_left_coset (a : α) : a ∈ a *l s :=
 suffices a * 1 ∈ a *l s, by simpa,
-mem_left_coset a (one_mem s)
+mem_left_coset a (one_mem s : 1 ∈ s)
 
 @[to_additive mem_own_right_add_coset]
 lemma mem_own_right_coset (a : α) : a ∈ (s : set α) *r a :=
 suffices 1 * a ∈ (s : set α) *r a, by simpa,
-mem_right_coset a (one_mem s)
+mem_right_coset a (one_mem s : 1 ∈ s)
 
 @[to_additive mem_left_add_coset_left_add_coset]
 lemma mem_left_coset_left_coset {a : α} (ha : a *l s = s) : a ∈ s :=
@@ -164,11 +164,11 @@ variables [group α] (s : subgroup α)
 
 @[to_additive left_add_coset_mem_left_add_coset]
 lemma left_coset_mem_left_coset {a : α} (ha : a ∈ s) : a *l s = s :=
-set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_left s (s.inv_mem ha)]
+set.ext $ by simp [mem_left_coset_iff, mul_mem_cancel_left (s.inv_mem ha)]
 
 @[to_additive right_add_coset_mem_right_add_coset]
 lemma right_coset_mem_right_coset {a : α} (ha : a ∈ s) : (s : set α) *r a = s :=
-set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_right s (s.inv_mem ha)]
+set.ext $ assume b, by simp [mem_right_coset_iff, mul_mem_cancel_right (s.inv_mem ha)]
 
 @[to_additive eq_add_cosets_of_normal]
 theorem eq_cosets_of_normal (N : s.normal) (g : α) : g *l s = s *r g :=
@@ -331,7 +331,7 @@ variables (s)
   stated in terms of an arbitrary `h : s`, rathern that the specific `h = g⁻¹ * (mk g).out'`. -/
 @[to_additive quotient_add_group.mk_out'_eq_mul]
 lemma mk_out'_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out' = g * h :=
-⟨⟨g⁻¹ * (mk g).out', eq'.mp (mk g).out_eq'.symm⟩, by rw [s.coe_mk, mul_inv_cancel_left]⟩
+⟨⟨g⁻¹ * (mk g).out', eq'.mp (mk g).out_eq'.symm⟩, by rw [set_like.coe_mk, mul_inv_cancel_left]⟩
 
 variables {s}
 
@@ -351,7 +351,7 @@ lemma preimage_image_coe (N : subgroup α) (s : set α) :
 begin
   ext x,
   simp only [quotient_group.eq, set_like.exists, exists_prop, set.mem_preimage, set.mem_Union,
-    set.mem_image, subgroup.coe_mk, ← eq_inv_mul_iff_mul_eq],
+    set.mem_image, set_like.coe_mk, ← eq_inv_mul_iff_mul_eq],
   exact ⟨λ ⟨y, hs, hN⟩, ⟨_, N.inv_mem hN, by simpa using hs⟩,
          λ ⟨z, hz, hxz⟩, ⟨x*z, hxz, by simpa using hz⟩⟩,
 end
@@ -416,7 +416,7 @@ def quotient_equiv_prod_of_le' (h_le : s ≤ t)
     rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left] }),
   left_inv := by
   { refine quotient.ind' (λ a, _),
-    simp_rw [quotient.map'_mk', id.def, t.coe_mk, mul_inv_cancel_left] },
+    simp_rw [quotient.map'_mk', id.def, set_like.coe_mk, mul_inv_cancel_left] },
   right_inv := by
   { refine prod.rec _,
     refine quotient.ind' (λ a, _),
diff --git a/src/group_theory/nilpotent.lean b/src/group_theory/nilpotent.lean
index db3e9199b0f78..77c70116bfa64 100644
--- a/src/group_theory/nilpotent.lean
+++ b/src/group_theory/nilpotent.lean
@@ -195,8 +195,7 @@ begin
   refine monotone_nat_of_le_succ _,
   intros n x hx y,
   rw [mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹],
-  exact mul_mem (upper_central_series G n) hx
-    (normal.conj_mem (upper_central_series.subgroup.normal G n) x⁻¹ (inv_mem _ hx) y),
+  exact mul_mem hx (normal.conj_mem (upper_central_series.subgroup.normal G n) x⁻¹ (inv_mem hx) y)
 end
 
 /-- A group `G` is nilpotent iff there exists an ascending central series which reaches `G` in
@@ -303,8 +302,7 @@ begin
     (@subgroup.inv_mem _ _ _),
   rintros y ⟨z, hz, a, ha⟩,
   rw [← ha, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹],
-  exact mul_mem (lower_central_series G n) hz
-    (normal.conj_mem (lower_central_series.subgroup.normal n) z⁻¹ (inv_mem _ hz) a),
+  exact mul_mem hz (normal.conj_mem (lower_central_series.subgroup.normal n) z⁻¹ (inv_mem hz) a)
 end
 
 /-- The lower central series of a group is a descending central series. -/
diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean
index 0601bcbd24878..6396adfaab898 100644
--- a/src/group_theory/order_of_element.lean
+++ b/src/group_theory/order_of_element.lean
@@ -741,9 +741,9 @@ have pow_mem : ∀ a : M, a ∈ S → ∀ n : ℕ, a ^ (n + 1) ∈ S :=
 def subgroup_of_idempotent {G : Type*} [group G] [fintype G] (S : set G)
   (hS1 : S.nonempty) (hS2 : S * S = S) : subgroup G :=
 { carrier := S,
-  inv_mem' := λ a ha, by
+  inv_mem' := λ a ha, show a⁻¹ ∈ submonoid_of_idempotent S hS1 hS2, by
   { rw [←one_mul a⁻¹, ←pow_one a, ←pow_order_of_eq_one a, ←pow_sub a (order_of_pos a)],
-    exact (submonoid_of_idempotent S hS1 hS2).pow_mem ha (order_of a - 1) },
+    exact pow_mem ha (order_of a - 1) },
   .. submonoid_of_idempotent S hS1 hS2 }
 
 /-- If `S` is a nonempty subset of a finite group `G`, then `S ^ |G|` is a subgroup -/
diff --git a/src/group_theory/perm/cycle_type.lean b/src/group_theory/perm/cycle_type.lean
index 906bdde3271bf..519190c9c6ec2 100644
--- a/src/group_theory/perm/cycle_type.lean
+++ b/src/group_theory/perm/cycle_type.lean
@@ -655,7 +655,7 @@ begin
   have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d),
   { simp [swap_comm c a, mul_assoc] },
   rw h',
-  exact mul_mem _ (swap_mul_swap_same_mem_closure_three_cycles ab ac)
+  exact mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
     (swap_mul_swap_same_mem_closure_three_cycles (ne.symm ac) cd),
 end
 
diff --git a/src/group_theory/specific_groups/alternating.lean b/src/group_theory/specific_groups/alternating.lean
index 880b4ce9afa67..e0905f2e65c9d 100644
--- a/src/group_theory/specific_groups/alternating.lean
+++ b/src/group_theory/specific_groups/alternating.lean
@@ -149,7 +149,7 @@ closure_eq_of_le _ (λ σ hσ, mem_alternating_group.2 hσ.sign) $ λ σ hσ, be
   obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn,
   rw [list.prod_cons, list.prod_cons, ← mul_assoc],
   rw [list.length_cons, nat.succ_inj'] at hn,
-  exact mul_mem _ (is_swap.mul_mem_closure_three_cycles (hl a (list.mem_cons_self a _))
+  exact mul_mem (is_swap.mul_mem_closure_three_cycles (hl a (list.mem_cons_self a _))
     (hl b (list.mem_cons_of_mem a (l.mem_cons_self b))))
     (ih _ (λ g hg, hl g (list.mem_cons_of_mem _ (list.mem_cons_of_mem _ hg))) hn),
 end
@@ -222,8 +222,8 @@ eq_top_iff.2 begin
   have h : (⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩ :
     alternating_group (fin 5)) ∈ normal_closure _ :=
     set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
-  exact mul_mem _ (subgroup.normal_closure_normal.conj_mem _ h
-    ⟨fin.cycle_range 2, fin.is_three_cycle_cycle_range_two.mem_alternating_group⟩) (inv_mem _ h),
+  exact mul_mem (subgroup.normal_closure_normal.conj_mem _ h
+    ⟨fin.cycle_range 2, fin.is_three_cycle_cycle_range_two.mem_alternating_group⟩) (inv_mem h),
 end
 
 /-- The normal closure of $(04)(13)$ within $A_5$ is the whole group. This will be
@@ -246,7 +246,7 @@ begin
   rw [set.singleton_subset_iff, set_like.mem_coe, ← h5],
   have h : g2 ∈ normal_closure {g2} :=
     set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
-  exact mul_mem _ (subgroup.normal_closure_normal.conj_mem _ h g1) (inv_mem _ h),
+  exact mul_mem (subgroup.normal_closure_normal.conj_mem _ h g1) (inv_mem h),
 end
 
 /-- Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps
@@ -321,7 +321,7 @@ instance is_simple_group_five : is_simple_group (alternating_group (fin 5)) :=
     refine normal_closure_le_normal _,
     rw [set.singleton_subset_iff, set_like.mem_coe],
     have h := set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
-    exact mul_mem _ h h },
+    exact mul_mem h h },
   { -- The case `n = 4` leads to contradiction, as no element of $A_5$ includes a 4-cycle.
     have con := mem_alternating_group.1 gA,
     contrapose! con,
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 0a4a608e99679..2f27617d09bca 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -95,10 +95,14 @@ section subgroup_class
 class inv_mem_class (S G : Type*) [has_inv G] [set_like S G] :=
 (inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s)
 
+export inv_mem_class (inv_mem)
+
 /-- `neg_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
 class neg_mem_class (S G : Type*) [has_neg G] [set_like S G] :=
 (neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s)
 
+export neg_mem_class (neg_mem)
+
 /-- `subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
 class subgroup_class (S G : Type*) [div_inv_monoid G] [set_like S G]
   extends submonoid_class S G :=
@@ -112,19 +116,15 @@ class add_subgroup_class (S G : Type*) [sub_neg_monoid G] [set_like S G]
 
 attribute [to_additive] inv_mem_class subgroup_class
 
-namespace subgroup_class
-
 variables (M S : Type*) [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M]
 include hSM
 
 @[to_additive, priority 100] -- See note [lower instance priority]
-instance to_inv_mem_class : inv_mem_class S M :=
+instance subgroup_class.to_inv_mem_class : inv_mem_class S M :=
 { .. hSM }
 
 variables {S M} {H K : S}
 
-open mul_mem_class inv_mem_class submonoid_class
-
 /-- A subgroup is closed under division. -/
 @[to_additive "An additive subgroup is closed under subtraction."]
 theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
@@ -162,6 +162,8 @@ lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
 lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
 ⟨λ hab, by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩
 
+namespace subgroup_class
+
 omit hSG
 include hSM
 
@@ -177,7 +179,7 @@ omit hSM
 /-- An additive subgroup of an `add_group` inherits an integer scaling. -/
 instance _root_.add_subgroup_class.has_zsmul {M S} [sub_neg_monoid M] [set_like S M]
   [add_subgroup_class S M] {H : S} : has_scalar ℤ H :=
-⟨λ n a, ⟨n • a, add_subgroup_class.zsmul_mem a.2 n⟩⟩
+⟨λ n a, ⟨n • a, zsmul_mem a.2 n⟩⟩
 include hSM
 
 /-- A subgroup of a group inherits an integer power. -/
@@ -420,54 +422,47 @@ theorem ext {H K : subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K := set_l
 
 /-- A subgroup contains the group's 1. -/
 @[to_additive "An `add_subgroup` contains the group's 0."]
-theorem one_mem : (1 : G) ∈ H := H.one_mem'
+protected theorem one_mem : (1 : G) ∈ H := one_mem _
 
 /-- A subgroup is closed under multiplication. -/
 @[to_additive "An `add_subgroup` is closed under addition."]
-theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H := λ hx hy, H.mul_mem' hx hy
+protected theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H := mul_mem
 
 /-- A subgroup is closed under inverse. -/
 @[to_additive "An `add_subgroup` is closed under inverse."]
-theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H := λ hx, H.inv_mem' hx
+protected theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H := inv_mem
 
 /-- A subgroup is closed under division. -/
 @[to_additive "An `add_subgroup` is closed under subtraction."]
-theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
-by simpa only [div_eq_mul_inv] using H.mul_mem' hx (H.inv_mem' hy)
+protected theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := div_mem hx hy
 
-@[simp, to_additive] theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
-⟨λ h, inv_inv x ▸ H.inv_mem h, H.inv_mem⟩
+@[to_additive] protected theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H := inv_mem_iff
 
-@[to_additive] lemma div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
-by rw [← H.inv_mem_iff, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev, inv_inv]
+@[to_additive] protected lemma div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
+div_mem_comm_iff
 
-@[simp, to_additive]
-theorem inv_coe_set : (H : set G)⁻¹ = H :=
-by { ext, simp, }
+@[to_additive] protected theorem inv_coe_set : (H : set G)⁻¹ = H := by { ext, simp }
 
-@[simp, to_additive]
-lemma exists_inv_mem_iff_exists_mem  (K : subgroup G) {P : G → Prop} :
+@[to_additive] protected lemma exists_inv_mem_iff_exists_mem  (K : subgroup G) {P : G → Prop} :
   (∃ (x : G), x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
-by split; { rintros ⟨x, x_in, hx⟩, exact ⟨x⁻¹, inv_mem K x_in, by simp [hx]⟩ }
+exists_inv_mem_iff_exists_mem
 
-@[to_additive]
-lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
-⟨λ hba, by simpa using H.mul_mem hba (H.inv_mem h), λ hb, H.mul_mem hb h⟩
+@[to_additive] protected lemma mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
+mul_mem_cancel_right h
 
-@[to_additive]
-lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
-⟨λ hab, by simpa using H.mul_mem (H.inv_mem h) hab, H.mul_mem h⟩
+@[to_additive] protected lemma mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
+mul_mem_cancel_left h
 
 /-- Product of a list of elements in a subgroup is in the subgroup. -/
 @[to_additive "Sum of a list of elements in an `add_subgroup` is in the `add_subgroup`."]
-lemma list_prod_mem {l : list G} : (∀ x ∈ l, x ∈ K) → l.prod ∈ K :=
-K.to_submonoid.list_prod_mem
+protected lemma list_prod_mem {l : list G} : (∀ x ∈ l, x ∈ K) → l.prod ∈ K :=
+list_prod_mem
 
 /-- Product of a multiset of elements in a subgroup of a `comm_group` is in the subgroup. -/
 @[to_additive "Sum of a multiset of elements in an `add_subgroup` of an `add_comm_group`
 is in the `add_subgroup`."]
-lemma multiset_prod_mem {G} [comm_group G] (K : subgroup G) (g : multiset G) :
-  (∀ a ∈ g, a ∈ K) → g.prod ∈ K := K.to_submonoid.multiset_prod_mem g
+protected lemma multiset_prod_mem {G} [comm_group G] (K : subgroup G) (g : multiset G) :
+  (∀ a ∈ g, a ∈ K) → g.prod ∈ K := multiset_prod_mem g
 
 @[to_additive]
 lemma multiset_noncomm_prod_mem (K : subgroup G) (g : multiset G)
@@ -479,10 +474,10 @@ K.to_submonoid.multiset_noncomm_prod_mem g comm
     subgroup. -/
 @[to_additive "Sum of elements in an `add_subgroup` of an `add_comm_group` indexed by a `finset`
 is in the `add_subgroup`."]
-lemma prod_mem {G : Type*} [comm_group G] (K : subgroup G)
+protected lemma prod_mem {G : Type*} [comm_group G] (K : subgroup G)
   {ι : Type*} {t : finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) :
   ∏ c in t, f c ∈ K :=
-K.to_submonoid.prod_mem h
+prod_mem h
 
 @[to_additive]
 lemma noncomm_prod_mem (K : subgroup G)
@@ -492,12 +487,10 @@ K.to_submonoid.noncomm_prod_mem t f comm
 
 
 @[to_additive add_subgroup.nsmul_mem]
-lemma pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K := K.to_submonoid.pow_mem hx
+protected lemma pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K := pow_mem hx
 
 @[to_additive]
-lemma zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
-| (n : ℕ) := by { rw [zpow_coe_nat], exact pow_mem _ hx n }
-| -[1+ n] := by { rw [zpow_neg_succ_of_nat], exact  K.inv_mem (K.pow_mem hx n.succ) }
+protected lemma zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K := zpow_mem hx
 
 /-- Construct a subgroup from a nonempty set that is closed under division. -/
 @[to_additive "Construct a subgroup from a nonempty set that is closed under subtraction"]
@@ -583,16 +576,16 @@ def subtype : H →* G := ⟨coe, rfl, λ _ _, rfl⟩
 
 @[simp, norm_cast, to_additive] theorem coe_list_prod (l : list H) :
   (l.prod : G) = (l.map coe).prod :=
-H.to_submonoid.coe_list_prod l
+submonoid_class.coe_list_prod l
 
 @[simp, norm_cast, to_additive] theorem coe_multiset_prod {G} [comm_group G] (H : subgroup G)
   (m : multiset H) : (m.prod : G) = (m.map coe).prod :=
-H.to_submonoid.coe_multiset_prod m
+submonoid_class.coe_multiset_prod m
 
 @[simp, norm_cast, to_additive] theorem coe_finset_prod {ι G} [comm_group G] (H : subgroup G)
   (f : ι → H) (s : finset ι) :
   ↑(∏ i in s, f i) = (∏ i in s, f i : G) :=
-H.to_submonoid.coe_finset_prod f s
+submonoid_class.coe_finset_prod f s
 
 /-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
 @[to_additive "The inclusion homomorphism from a additive subgroup `H` contained in `K` to `K`."]
@@ -860,8 +853,8 @@ lemma closure_induction {p : G → Prop} {x} (h : x ∈ closure k)
 lemma closure_induction' {p : Π x, x ∈ closure k → Prop}
   (Hs : ∀ x (h : x ∈ k), p x (subset_closure h))
   (H1 : p 1 (one_mem _))
-  (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem _ hx hy))
-  (Hinv : ∀ x hx, p x hx → p x⁻¹ (inv_mem _ hx))
+  (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
+  (Hinv : ∀ x hx, p x hx → p x⁻¹ (inv_mem hx))
   {x} (hx : x ∈ closure k) :
   p x hx :=
 begin
@@ -892,8 +885,8 @@ eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
   refine closure_induction' (λ g hg, _) _ (λ g₁ g₂ hg₁ hg₂, _) (λ g hg, _) hx,
   { exact subset_closure hg },
   { exact one_mem _ },
-  { exact mul_mem _ },
-  { exact inv_mem _ }
+  { exact mul_mem },
+  { exact inv_mem }
 end
 
 /-- If all the elements of a set `s` commute, then `closure s` is a commutative group. -/
@@ -969,7 +962,7 @@ natural number multiples of the element."-/]
 lemma mem_closure_singleton {x y : G} : y ∈ closure ({x} : set G) ↔ ∃ n : ℤ, x ^ n = y :=
 begin
   refine ⟨λ hy, closure_induction hy _ _ _ _,
-    λ ⟨n, hn⟩, hn ▸ zpow_mem _ (subset_closure $ mem_singleton x) n⟩,
+    λ ⟨n, hn⟩, hn ▸ zpow_mem (subset_closure $ mem_singleton x) n⟩,
   { intros y hy,
     rw [eq_of_mem_singleton hy],
     exact ⟨1, zpow_one x⟩ },
@@ -1051,7 +1044,7 @@ begin
   { obtain ⟨i, hi⟩ := set.mem_Union.mp hx,
     exact hp _ _ hi, },
   { obtain ⟨i, hi⟩ := set.mem_Union.mp hx,
-    exact hp _ _ (inv_mem _ hi), },
+    exact hp _ _ (inv_mem hi), },
 end
 
 /-- A dependent version of `subgroup.supr_induction`. -/
@@ -1059,7 +1052,7 @@ end
 lemma supr_induction' {ι : Sort*} (S : ι → subgroup G) {C : Π x, (x ∈ ⨆ i, S i) → Prop}
   (hp : ∀ i (x ∈ S i), C x (mem_supr_of_mem i ‹_›))
   (h1 : C 1 (one_mem _))
-  (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem _ ‹_› ‹_›))
+  (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›))
   {x : G} (hx : x ∈ ⨆ i, S i) : C x hx :=
 begin
   refine exists.elim _ (λ (hx : x ∈ ⨆ i, S i) (hc : C x hx), hc),
@@ -1082,8 +1075,8 @@ begin
   { exact hι.elim (λ i, ⟨i, (K i).one_mem⟩) },
   { rintros x y ⟨i, hi⟩ ⟨j, hj⟩,
     rcases hK i j with ⟨k, hki, hkj⟩,
-    exact ⟨k, (K k).mul_mem (hki hi) (hkj hj)⟩ },
-    rintros _ ⟨i, hi⟩, exact ⟨i, inv_mem (K i) hi⟩
+    exact ⟨k, mul_mem (hki hi) (hkj hj)⟩ },
+    rintros _ ⟨i, hi⟩, exact ⟨i, inv_mem hi⟩
 end
 
 @[to_additive]
@@ -1438,9 +1431,9 @@ lemma pi_mem_of_mul_single_mem_aux [decidable_eq η] (I : finset η) {H : subgro
   x ∈ H :=
 begin
   induction I using finset.induction_on with i I hnmem ih generalizing x,
-  { have : x = 1,
-    { ext i, refine (h1 i (not_mem_empty i)), },
-    simp [this, one_mem], },
+  { convert one_mem H,
+    ext i,
+    exact (h1 i (not_mem_empty i)) },
   { have : x = function.update x i 1 * pi.mul_single i (x i),
     { ext j,
       by_cases heq : j = i,
@@ -1884,9 +1877,9 @@ begin
   { exact (conjugates_of_set_subset_normal_closure (conj_mem_conjugates_of_set hx)) },
   { simpa using (normal_closure s).one_mem },
   { rw ← conj_mul,
-    exact mul_mem _ ihx ihy },
+    exact mul_mem ihx ihy },
   { rw ← conj_inv,
-    exact inv_mem _ ihx }
+    exact inv_mem ihx }
 end⟩
 
 /-- The normal closure of `s` is the smallest normal subgroup containing `s`. -/
@@ -1896,9 +1889,9 @@ begin
   assume a w,
   refine closure_induction w (λ x hx, _) _  (λ x y ihx ihy, _) (λ x ihx, _),
   { exact (conjugates_of_set_subset h hx) },
-  { exact subgroup.one_mem _ },
-  { exact subgroup.mul_mem _ ihx ihy },
-  { exact subgroup.inv_mem _ ihx }
+  { exact one_mem _ },
+  { exact mul_mem ihx ihy },
+  { exact inv_mem ihx }
 end
 
 lemma normal_closure_subset_iff {N : subgroup G} [N.normal] : s ⊆ N ↔ normal_closure s ≤ N :=
@@ -2713,9 +2706,9 @@ lemma mem_sup : x ∈ s ⊔ t ↔ ∃ (y ∈ s) (z ∈ t), y * z = x :=
     { exact ⟨1, s.one_mem, y, h, by simp⟩ } },
   { exact ⟨1, s.one_mem, 1, ⟨t.one_mem, mul_one 1⟩⟩ },
   { rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩,
-    exact ⟨_, mul_mem _ hy₁ hy₂, _, mul_mem _ hz₁ hz₂, by simp [mul_assoc]; cc⟩ },
+    exact ⟨_, mul_mem hy₁ hy₂, _, mul_mem hz₁ hz₂, by simp [mul_assoc]; cc⟩ },
   { rintro _ ⟨y, hy, z, hz, rfl⟩,
-    exact ⟨_, inv_mem _ hy, _, inv_mem _ hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩ }
+    exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩ }
 end, by rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz⟩
 
 @[to_additive]
@@ -2853,12 +2846,12 @@ begin
   simp only [coe_inf, set.inf_eq_inter, set.mem_mul, set.mem_inter_iff],
   split,
   { rintros ⟨y, z, hy, ⟨hzB, hzC⟩, rfl⟩,
-    refine ⟨_, mul_mem C (h hy) hzC⟩,
+    refine ⟨_, mul_mem (h hy) hzC⟩,
     exact ⟨y, z, hy, hzB, rfl⟩ },
   rintros ⟨⟨y, z, hy, hz, rfl⟩, hyz⟩,
   refine ⟨y, z, hy, ⟨hz, _⟩, rfl⟩,
   suffices : y⁻¹ * (y * z) ∈ C, { simpa },
-  exact mul_mem C (inv_mem C (h hy)) hyz
+  exact mul_mem (inv_mem (h hy)) hyz
 end
 
 @[to_additive] lemma inf_mul_assoc (A B C : subgroup G) (h : C ≤ A) :
@@ -2868,12 +2861,12 @@ begin
   simp only [coe_inf, set.inf_eq_inter, set.mem_mul, set.mem_inter_iff],
   split,
   { rintros ⟨y, z, ⟨hyA, hyB⟩, hz, rfl⟩,
-    refine ⟨mul_mem A hyA (h hz), _⟩,
+    refine ⟨A.mul_mem hyA (h hz), _⟩,
     exact ⟨y, z, hyB, hz, rfl⟩ },
   rintros ⟨hyz, y, z, hy, hz, rfl⟩,
   refine ⟨y, z, ⟨_, hy⟩, hz, rfl⟩,
   suffices : (y * z) * z⁻¹ ∈ A, { simpa },
-  exact mul_mem A hyz (inv_mem A (h hz))
+  exact mul_mem hyz (inv_mem (h hz))
 end
 
 end pointwise
@@ -2906,7 +2899,7 @@ section subgroup_normal
   (A B' B : subgroup G) (hB : B' ≤ B) [hN : (B'.subgroup_of B).normal] :
   ((A ⊓ B').subgroup_of (A ⊓ B)).normal :=
 { conj_mem := λ n hn g,
-    ⟨mul_mem A (mul_mem A (mem_inf.1 g.2).1 (mem_inf.1 n.2).1) (inv_mem A (mem_inf.1 g.2).1),
+    ⟨mul_mem (mul_mem (mem_inf.1 g.2).1 (mem_inf.1 n.2).1) (inv_mem (mem_inf.1 g.2).1),
     (normal_subgroup_of_iff hB).mp hN n g hn.2 (mem_inf.mp g.2).2⟩ }
 
 @[to_additive] lemma inf_subgroup_of_inf_normal_of_left
@@ -2914,7 +2907,7 @@ section subgroup_normal
   ((A' ⊓ B).subgroup_of (A ⊓ B)).normal :=
 { conj_mem := λ n hn g,
     ⟨(normal_subgroup_of_iff hA).mp hN n g hn.1  (mem_inf.mp g.2).1,
-    mul_mem B (mul_mem B (mem_inf.1 g.2).2 (mem_inf.1 n.2).2) (inv_mem B (mem_inf.1 g.2).2)⟩ }
+    mul_mem (mul_mem (mem_inf.1 g.2).2 (mem_inf.1 n.2).2) (inv_mem (mem_inf.1 g.2).2)⟩ }
 
 instance sup_normal (H K : subgroup G) [hH : H.normal] [hK : K.normal] : (H ⊔ K).normal :=
 { conj_mem := λ n hmem g,
diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean
index 64bae1284a465..9693929f3f6e7 100644
--- a/src/group_theory/submonoid/basic.lean
+++ b/src/group_theory/submonoid/basic.lean
@@ -61,14 +61,20 @@ variables [add_zero_class A] {t : set A}
 class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] :=
 (one_mem : ∀ (s : S), (1 : M) ∈ s)
 
+export one_mem_class (one_mem)
+
 /-- `zero_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/
 class zero_mem_class (S : Type*) (M : out_param $ Type*) [has_zero M] [set_like S M] :=
 (zero_mem : ∀ (s : S), (0 : M) ∈ s)
 
+export zero_mem_class (zero_mem)
+
 /-- `mul_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(*)` -/
 class mul_mem_class (S : Type*) (M : out_param $ Type*) [has_mul M] [set_like S M] :=
 (mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s)
 
+export mul_mem_class (mul_mem)
+
 /-- `add_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(+)` -/
 class add_mem_class (S : Type*) (M : out_param $ Type*) [has_add M] [set_like S M] :=
 (add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s)
@@ -186,11 +192,11 @@ variable (S)
 
 /-- A submonoid contains the monoid's 1. -/
 @[to_additive "An `add_submonoid` contains the monoid's 0."]
-theorem one_mem : (1 : M) ∈ S := S.one_mem'
+protected theorem one_mem : (1 : M) ∈ S := one_mem S
 
 /-- A submonoid is closed under multiplication. -/
 @[to_additive "An `add_submonoid` is closed under addition."]
-theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S := submonoid.mul_mem' S
+protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S := mul_mem
 
 /-- The submonoid `M` of the monoid `M`. -/
 @[to_additive "The additive submonoid `M` of the `add_monoid M`."]
@@ -343,7 +349,7 @@ lemma closure_induction {p : M → Prop} {x} (h : x ∈ closure s)
 lemma closure_induction' (s : set M) {p : Π x, x ∈ closure s → Prop}
   (Hs : ∀ x (h : x ∈ s), p x (subset_closure h))
   (H1 : p 1 (one_mem _))
-  (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem _ hx hy))
+  (Hmul : ∀ x hx y hy, p x hx → p y hy → p (x * y) (mul_mem hx hy))
   {x} (hx : x ∈ closure s) :
   p x hx :=
 begin
diff --git a/src/group_theory/submonoid/membership.lean b/src/group_theory/submonoid/membership.lean
index 3ca8561687b5c..b740035c5d85a 100644
--- a/src/group_theory/submonoid/membership.lean
+++ b/src/group_theory/submonoid/membership.lean
@@ -54,6 +54,10 @@ namespace submonoid_class
   ↑(∏ i in s, f i) = (∏ i in s, f i : M) :=
 (submonoid_class.subtype S : _ →* M).map_prod f s
 
+end submonoid_class
+
+open submonoid_class
+
 /-- Product of a list of elements in a submonoid is in the submonoid. -/
 @[to_additive "Sum of a list of elements in an `add_submonoid` is in the `add_submonoid`."]
 lemma list_prod_mem {l : list M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S :=
@@ -75,8 +79,6 @@ lemma prod_mem {M : Type*} [comm_monoid M] [set_like B M] [submonoid_class B M]
   ∏ c in t, f c ∈ S :=
 multiset_prod_mem (t.1.map f) $ λ x hx, let ⟨i, hi, hix⟩ := multiset.mem_map.1 hx in hix ▸ h i hi
 
-end submonoid_class
-
 namespace submonoid
 
 variables (s : submonoid M)
@@ -229,7 +231,7 @@ end
 lemma supr_induction' {ι : Sort*} (S : ι → submonoid M) {C : Π x, (x ∈ ⨆ i, S i) → Prop}
   (hp : ∀ i (x ∈ S i), C x (mem_supr_of_mem i ‹_›))
   (h1 : C 1 (one_mem _))
-  (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem _ ‹_› ‹_›))
+  (hmul : ∀ x y hx hy, C x hx → C y hy → C (x * y) (mul_mem ‹_› ‹_›))
   {x : M} (hx : x ∈ ⨆ i, S i) : C x hx :=
 begin
   refine exists.elim _ (λ (hx : x ∈ ⨆ i, S i) (hc : C x hx), hc),
@@ -253,7 +255,7 @@ open submonoid
 @[to_additive]
 theorem closure_range_of : closure (set.range $ @of α) = ⊤ :=
 eq_top_iff.2 $ λ x hx, free_monoid.rec_on x (one_mem _) $ λ x xs hxs,
-  mul_mem _ (subset_closure $ set.mem_range_self _) hxs
+  mul_mem (subset_closure $ set.mem_range_self _) hxs
 
 end free_monoid
 
@@ -265,7 +267,7 @@ open monoid_hom
 
 lemma closure_singleton_eq (x : M) : closure ({x} : set M) = (powers_hom M x).mrange :=
 closure_eq_of_le (set.singleton_subset_iff.2 ⟨multiplicative.of_add 1, pow_one x⟩) $
-  λ x ⟨n, hn⟩, hn ▸ submonoid.pow_mem _ (subset_closure $ set.mem_singleton _) _
+  λ x ⟨n, hn⟩, hn ▸ pow_mem (subset_closure $ set.mem_singleton _) _
 
 /-- The submonoid generated by an element of a monoid equals the set of natural number powers of
     the element. -/
@@ -315,7 +317,7 @@ end
 lemma closure_induction_right {s : set M} {p : M → Prop} {x : M} (h : x ∈ closure s) (H1 : p 1)
   (Hmul : ∀ x (y ∈ s), p x → p (x * y)) : p x :=
 @closure_induction_left _ _ (mul_opposite.unop ⁻¹' s) (p ∘ mul_opposite.unop) (mul_opposite.op x)
-  (closure_induction h (λ x hx, subset_closure hx) (one_mem _) (λ x y hx hy, mul_mem _ hy hx))
+  (closure_induction h (λ x hx, subset_closure hx) (one_mem _) (λ x y hx hy, mul_mem hy hx))
   H1 (λ x hx y, Hmul _ _ hx)
 
 /-- The submonoid generated by an element. -/
@@ -331,7 +333,7 @@ lemma powers_eq_closure (n : M) : powers n = closure {n} :=
 by { ext, exact mem_closure_singleton.symm }
 
 lemma powers_subset {n : M} {P : submonoid M} (h : n ∈ P) : powers n ≤ P :=
-λ x hx, match x, hx with _, ⟨i, rfl⟩ := P.pow_mem h i end
+λ x hx, match x, hx with _, ⟨i, rfl⟩ := pow_mem h i end
 
 /-- Exponentiation map from natural numbers to powers. -/
 @[simps] def pow (n : M) (m : ℕ) : powers n :=
@@ -421,7 +423,7 @@ open set
 
 lemma closure_singleton_eq (x : A) : closure ({x} : set A) = (multiples_hom A x).mrange :=
 closure_eq_of_le (set.singleton_subset_iff.2 ⟨1, one_nsmul x⟩) $
-  λ x ⟨n, hn⟩, hn ▸ nsmul_mem _ (subset_closure $ set.mem_singleton _) _
+  λ x ⟨n, hn⟩, hn ▸ nsmul_mem (subset_closure $ set.mem_singleton _) _
 
 /-- The `add_submonoid` generated by an element of an `add_monoid` equals the set of
 natural number multiples of the element. -/
@@ -445,7 +447,7 @@ lemma multiples_eq_closure (x : A) : multiples x = closure {x} :=
 by { ext, exact mem_closure_singleton.symm }
 
 lemma multiples_subset {x : A} {P : add_submonoid A} (h : x ∈ P) : multiples x ≤ P :=
-λ x hx, match x, hx with _, ⟨i, rfl⟩ := P.nsmul_mem h i end
+λ x hx, match x, hx with _, ⟨i, rfl⟩ := nsmul_mem h i end
 
 attribute [to_additive add_submonoid.multiples] submonoid.powers
 attribute [to_additive add_submonoid.mem_multiples] submonoid.mem_powers
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
index dca7f7c9d5413..43646c13d52db 100644
--- a/src/group_theory/submonoid/operations.lean
+++ b/src/group_theory/submonoid/operations.lean
@@ -385,8 +385,6 @@ namespace submonoid_class
 variables {A : Type*} [set_like A M] [hA : submonoid_class A M] (S' : A)
 include hA
 
-open mul_mem_class
-
 /-- A submonoid of a monoid inherits a multiplication. -/
 @[to_additive "An `add_submonoid` of an `add_monoid` inherits an addition."]
 instance has_mul : has_mul S' := ⟨λ a b, ⟨a.1 * b.1, mul_mem a.2 b.2⟩⟩
@@ -528,18 +526,10 @@ structure."]
 instance to_mul_one_class {M : Type*} [mul_one_class M] (S : submonoid M) : mul_one_class S :=
 subtype.coe_injective.mul_one_class coe rfl (λ _ _, rfl)
 
-@[to_additive] lemma pow_mem {M : Type*} [monoid M] (S : submonoid M) {x : M}
+@[to_additive] protected lemma pow_mem {M : Type*} [monoid M] (S : submonoid M) {x : M}
   (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S :=
 pow_mem hx n
 
-instance _root_.add_submonoid.has_nsmul {M : Type*} [add_monoid M] (S : add_submonoid M) :
-  has_scalar ℕ S :=
-⟨λ n x, ⟨n • x, S.nsmul_mem x.prop _⟩⟩
-
-@[to_additive]
-instance has_pow {M : Type*} [monoid M] (S : submonoid M) : has_pow S ℕ :=
-⟨λ x n, ⟨x ^ n, S.pow_mem x.prop _⟩⟩
-
 @[simp, norm_cast, to_additive] theorem coe_pow  {M : Type*} [monoid M] {S : submonoid M}
   (x : S) (n : ℕ) : ↑(x ^ n) = (x ^ n : M) :=
 rfl
@@ -685,7 +675,7 @@ ext $ λ p, ⟨λ ⟨x, hx, hp⟩, hp ▸ ⟨set.mem_singleton 1, hx⟩,
 lemma prod_bot_sup_bot_prod (s : submonoid M) (t : submonoid N) :
   (s.prod ⊥) ⊔ (prod ⊥ t) = s.prod t :=
 le_antisymm (sup_le (prod_mono (le_refl s) bot_le) (prod_mono bot_le (le_refl t))) $
-assume p hp, prod.fst_mul_snd p ▸ mul_mem _
+assume p hp, prod.fst_mul_snd p ▸ mul_mem
   ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, set.mem_singleton 1⟩)
   ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨set.mem_singleton 1, hp.2⟩)
 
diff --git a/src/group_theory/submonoid/pointwise.lean b/src/group_theory/submonoid/pointwise.lean
index ee54fbc21b711..70c9ecdfb7c44 100644
--- a/src/group_theory/submonoid/pointwise.lean
+++ b/src/group_theory/submonoid/pointwise.lean
@@ -344,7 +344,8 @@ begin
       work_on_goal 1 { intros, exact subset_closure ⟨_, _, ‹_›, ‹_›, rfl⟩ } },
     all_goals { intros, simp only [mul_zero, zero_mul, zero_mem,
         left_distrib, right_distrib, mul_smul_comm, smul_mul_assoc],
-      try {apply add_mem _ _ _}, try {apply smul_mem _ _ _} }, assumption' },
+      solve_by_elim [add_mem _ _, zero_mem _]
+        { max_depth := 4, discharger := tactic.interactive.apply_instance } } },
   { rw closure_le, rintros _ ⟨a, b, ha, hb, rfl⟩,
     exact mul_mem_mul (subset_closure ha) (subset_closure hb) }
 end
diff --git a/src/group_theory/sylow.lean b/src/group_theory/sylow.lean
index ef8665efcf2a4..6162d38e67c71 100644
--- a/src/group_theory/sylow.lean
+++ b/src/group_theory/sylow.lean
@@ -303,7 +303,7 @@ lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G}
   (x : G ⧸ H) ∈ fixed_points H (G ⧸ H) ↔ x ∈ normalizer H :=
 ⟨λ hx, have ha : ∀ {y : G ⧸ H}, y ∈ orbit H (x : G ⧸ H) → y = x,
   from λ _, ((mem_fixed_points' _).1 hx _),
-  (inv_mem_iff _).1 (@mem_normalizer_fintype _ _ _ _inst_2 _ (λ n (hn : n ∈ H),
+  inv_mem_iff.1 (@mem_normalizer_fintype _ _ _ _inst_2 _ (λ n (hn : n ∈ H),
     have (n⁻¹ * x)⁻¹ * x ∈ H := quotient_group.eq.1 (ha (mem_orbit _ ⟨n⁻¹, H.inv_mem hn⟩)),
     show _ ∈ H, by {rw [mul_inv_rev, inv_inv] at this, convert this, rw inv_inv}
     )),
@@ -311,7 +311,7 @@ lemma mem_fixed_points_mul_left_cosets_iff_mem_normalizer {H : subgroup G}
 (mem_fixed_points' _).2 $ λ y, quotient.induction_on' y $ λ y hy, quotient_group.eq.2
   (let ⟨⟨b, hb₁⟩, hb₂⟩ := hy in
   have hb₂ : (b * x)⁻¹ * y ∈ H := quotient_group.eq.1 hb₂,
-  (inv_mem_iff H).1 $ (hx _).2 $ (mul_mem_cancel_left H (H.inv_mem hb₁)).1
+  inv_mem_iff.1 $ (hx _).2 $ (mul_mem_cancel_left (inv_mem hb₁)).1
   $ by rw hx at hb₂;
     simpa [mul_inv_rev, mul_assoc] using hb₂)⟩
 
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index a686d17fdc63f..03ed05e23ccec 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -805,8 +805,8 @@ variables [add_comm_group M₂] [module R M₂]
 @[simp] lemma neg_coe : -(p : set M) = p := set.ext $ λ x, p.neg_mem_iff
 
 @[simp] protected lemma map_neg (f : M →ₗ[R] M₂) : map (-f) p = map f p :=
-ext $ λ y, ⟨λ ⟨x, hx, hy⟩, hy ▸ ⟨-x, neg_mem _ hx, f.map_neg x⟩,
-  λ ⟨x, hx, hy⟩, hy ▸ ⟨-x, neg_mem _ hx, ((-f).map_neg _).trans (neg_neg (f x))⟩⟩
+ext $ λ y, ⟨λ ⟨x, hx, hy⟩, hy ▸ ⟨-x, show -x ∈ p, from neg_mem hx, map_neg f x⟩,
+  λ ⟨x, hx, hy⟩, hy ▸ ⟨-x, show -x ∈ p, from neg_mem hx, (map_neg (-f) _).trans (neg_neg (f x))⟩⟩
 
 end add_comm_group
 
@@ -1118,7 +1118,7 @@ by rw [mem_ker, map_sub, sub_eq_zero]
 theorem disjoint_ker' {p : submodule R M} :
   disjoint p (ker f) ↔ ∀ x y ∈ p, f x = f y → x = y :=
 disjoint_ker.trans
-⟨λ H x hx y hy h, eq_of_sub_eq_zero $ H _ (sub_mem _ hx hy) (by simp [h]),
+⟨λ H x hx y hy h, eq_of_sub_eq_zero $ H _ (sub_mem hx hy) (by simp [h]),
  λ H x h₁ h₂, H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩
 
 theorem inj_of_disjoint_ker {p : submodule R M}
@@ -1403,10 +1403,14 @@ def submodule_map (p : submodule R M) :
 { inv_fun   := λ y, ⟨(e.symm : M₂ →ₛₗ[σ₂₁] M) y, by
   { rcases y with ⟨y', hy⟩, rw submodule.mem_map at hy, rcases hy with ⟨x, hx, hxy⟩, subst hxy,
     simp only [symm_apply_apply, submodule.coe_mk, coe_coe, hx], }⟩,
-  left_inv  := λ x, by simp,
-  right_inv := λ y, by { apply set_coe.ext, simp, },
+  left_inv  := λ x, by simp only [linear_map.dom_restrict_apply, linear_map.cod_restrict_apply,
+    linear_map.to_fun_eq_coe, linear_equiv.coe_coe, linear_equiv.symm_apply_apply, set_like.eta],
+  right_inv := λ y, by { apply set_coe.ext, simp only [linear_map.dom_restrict_apply,
+    linear_map.cod_restrict_apply, linear_map.to_fun_eq_coe, linear_equiv.coe_coe, set_like.coe_mk,
+    linear_equiv.apply_symm_apply] },
   ..((e : M →ₛₗ[σ₁₂] M₂).dom_restrict p).cod_restrict (p.map (e : M →ₛₗ[σ₁₂] M₂))
-  (λ x, ⟨x, by simp⟩) }
+  (λ x, ⟨x, by simp only [linear_map.dom_restrict_apply, eq_self_iff_true, and_true,
+                          set_like.coe_mem, set_like.mem_coe]⟩) }
 
 include σ₂₁
 @[simp] lemma submodule_map_apply (p : submodule R M) (x : p) :
diff --git a/src/linear_algebra/dfinsupp.lean b/src/linear_algebra/dfinsupp.lean
index 7543bb2374b7a..230147f10ca12 100644
--- a/src/linear_algebra/dfinsupp.lean
+++ b/src/linear_algebra/dfinsupp.lean
@@ -229,12 +229,12 @@ open dfinsupp
 lemma dfinsupp_sum_mem {β : ι → Type*} [Π i, has_zero (β i)]
   [Π i (x : β i), decidable (x ≠ 0)] (S : submodule R N)
   (f : Π₀ i, β i) (g : Π i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
-S.to_add_submonoid.dfinsupp_sum_mem f g h
+dfinsupp_sum_mem S f g h
 
 lemma dfinsupp_sum_add_hom_mem {β : ι → Type*} [Π i, add_zero_class (β i)]
   (S : submodule R N) (f : Π₀ i, β i) (g : Π i, β i →+ N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
   dfinsupp.sum_add_hom g f ∈ S :=
-S.to_add_submonoid.dfinsupp_sum_add_hom_mem f g h
+dfinsupp_sum_add_hom_mem S f g h
 
 /-- The supremum of a family of submodules is equal to the range of `dfinsupp.lsum`; that is
 every element in the `supr` can be produced from taking a finite number of non-zero elements
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index a7f2122294d96..0970b2dc6d996 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -1293,7 +1293,7 @@ begin
   -- To show `b i ∈ span (b '' (univ \ {i}))`, we use that it's a weighted sum
   -- of the other `b j`s.
   rw [j_eq, set_like.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum (λ j, g j • b j)), from _],
-  { refine submodule.neg_mem _ (smul_mem _ _ (sum_mem _ (λ k hk, _))),
+  { refine neg_mem (smul_mem _ _ (sum_mem (λ k hk, _))),
     obtain ⟨k_ne_i, k_mem⟩ := finset.mem_erase.mp hk,
     refine smul_mem _ _ (subset_span ⟨k, _, rfl⟩),
     simpa using k_mem },
diff --git a/src/linear_algebra/finsupp.lean b/src/linear_algebra/finsupp.lean
index 3b3504f623204..9587014561904 100644
--- a/src/linear_algebra/finsupp.lean
+++ b/src/linear_algebra/finsupp.lean
@@ -129,7 +129,7 @@ lemma supr_lsingle_range : (⨆a, (lsingle a : M →ₗ[R] (α →₀ M)).range)
 begin
   refine (eq_top_iff.2 $ set_like.le_def.2 $ assume f _, _),
   rw [← sum_single f],
-  exact sum_mem _ (assume a ha, submodule.mem_supr_of_mem a ⟨_, rfl⟩),
+  exact sum_mem (assume a ha, submodule.mem_supr_of_mem a ⟨_, rfl⟩),
 end
 
 lemma disjoint_lsingle_lsingle (s t : set α) (hs : disjoint s t) :
@@ -191,7 +191,7 @@ begin
   refine (span_eq_of_le _ _ (set_like.le_def.2 $ λ l hl, _)).symm,
   { rintro _ ⟨_, hp, rfl ⟩ , exact single_mem_supported R 1 hp },
   { rw ← l.sum_single,
-    refine sum_mem _ (λ i il, _),
+    refine sum_mem (λ i il, _),
     convert @smul_mem R (α →₀ R) _ _ _ _ (single i 1) (l i) _,
     { simp },
     apply subset_span,
@@ -249,8 +249,8 @@ begin
   { rwa [linear_map.range_comp, range_restrict_dom, map_top, range_subtype] at this },
   rw [range_le_iff_comap, eq_top_iff],
   rintro l ⟨⟩,
-  apply finsupp.induction l, {exact zero_mem _},
-  refine λ x a l hl a0, add_mem _ _,
+  apply finsupp.induction l, { exact zero_mem _ },
+  refine λ x a l hl a0, add_mem _,
   by_cases (∃ i, x ∈ s i); simp [h],
   { cases h with i hi,
     exact le_supr (λ i, supported M R (s i)) i (single_mem_supported R _ hi) }
@@ -466,9 +466,7 @@ begin
     rcases hx with ⟨l, hl⟩,
     rw ← hl,
     rw finsupp.total_apply,
-    unfold finsupp.sum,
-    apply sum_mem (span R (range v)),
-    exact λ i hi, submodule.smul_mem _ _ (subset_span (mem_range_self i)) },
+    exact sum_mem (λ i hi, submodule.smul_mem _ _ (subset_span (mem_range_self i))) },
   { apply span_le.2,
     intros x hx,
     rcases hx with ⟨i, hi⟩,
@@ -524,7 +522,7 @@ begin
       by_cases c ∈ s,
       { exact smul_mem _ _ (subset_span (set.mem_image_of_mem _ h)) },
       { simp [(finsupp.mem_supported' R _).1 hz _ h] } },
-    refine sum_mem _ _, simp [this] }
+    refine sum_mem _, simp [this] }
 end
 
 theorem mem_span_image_iff_total {s : set α} {x : M} :
@@ -844,9 +842,9 @@ attribute [irreducible] span.repr
 
 end
 
-lemma submodule.finsupp_sum_mem {ι β : Type*} [has_zero β] (S : submodule R M) (f : ι →₀ β)
-  (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
-S.to_add_submonoid.finsupp_sum_mem f g h
+protected lemma submodule.finsupp_sum_mem {ι β : Type*} [has_zero β] (S : submodule R M)
+  (f : ι →₀ β) (g : ι → β → M) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S :=
+add_submonoid_class.finsupp_sum_mem S f g h
 
 lemma linear_map.map_finsupp_total
   (f : M →ₗ[R] N) {ι : Type*} {g : ι → M} (l : ι →₀ R) :
@@ -892,7 +890,7 @@ lemma mem_span_finset {s : finset M} {x : M} :
 ⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_image_iff_total _).1
     (show x ∈ span R (id '' (↑s : set M)), by rwa set.image_id) in
   ⟨v, hvx ▸ (finsupp.total_apply_of_mem_supported _ hvs).symm⟩,
-λ ⟨f, hf⟩, hf ▸ sum_mem _ (λ i hi, smul_mem _ _ $ subset_span hi)⟩
+λ ⟨f, hf⟩, hf ▸ sum_mem (λ i hi, smul_mem _ _ $ subset_span hi)⟩
 
 /-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
 `m` can be written as a finite `R`-linear combination of elements of `s`.
diff --git a/src/linear_algebra/linear_independent.lean b/src/linear_algebra/linear_independent.lean
index a2fe1b092b63d..19fac22920bc8 100644
--- a/src/linear_algebra/linear_independent.lean
+++ b/src/linear_algebra/linear_independent.lean
@@ -262,7 +262,7 @@ begin
   forall_true_iff, imp_self, fin.succ_inj, finset.sum_image] at total_eq,
   have : g 0 = 0,
   { refine x_ortho (g 0) ⟨∑ (i : fin m), g i.succ • v i, _⟩ total_eq,
-    exact sum_mem _ (λ i _, smul_mem _ _ (subset_span ⟨i, rfl⟩)) },
+    exact sum_mem (λ i _, smul_mem _ _ (subset_span ⟨i, rfl⟩)) },
   refine fin.cases this (λ j, _) j,
   apply hli (λ i, g i.succ),
   simpa only [this, zero_smul, zero_add] using total_eq
@@ -626,7 +626,7 @@ begin
     { exact finset.disjoint_filter.2 (λ x hx, disjoint_left.1 is_compl_range_inl_range_inr.1) } },
   { rw ← eq_neg_iff_add_eq_zero at this,
     rw [disjoint_def'] at hlr,
-    have A := hlr _ (sum_mem _ $ λ i hi, _) _ (neg_mem _ $ sum_mem _ $ λ i hi, _) this,
+    have A := hlr _ (sum_mem $ λ i hi, _) _ (neg_mem $ sum_mem $ λ i hi, _) this,
     { cases i with i i,
       { exact hl _ _ A i (finset.mem_preimage.2 hi) },
       { rw [this, neg_eq_zero] at A,
@@ -700,21 +700,22 @@ variables (hv : linear_independent R v)
 
 /-- Canonical isomorphism between linear combinations and the span of linearly independent vectors.
 -/
-@[simps] def linear_independent.total_equiv (hv : linear_independent R v) :
+@[simps {rhs_md := semireducible}]
+def linear_independent.total_equiv (hv : linear_independent R v) :
   (ι →₀ R) ≃ₗ[R] span R (range v) :=
 begin
-apply linear_equiv.of_bijective
-  (linear_map.cod_restrict (span R (range v)) (finsupp.total ι M R v) _),
-{ rw [← linear_map.ker_eq_bot, linear_map.ker_cod_restrict],
-  apply hv },
-{ rw [← linear_map.range_eq_top, linear_map.range_eq_map, linear_map.map_cod_restrict,
-    ← linear_map.range_le_iff_comap, range_subtype, map_top],
-  rw finsupp.range_total,
-  exact le_rfl },
-{ intro l,
-  rw ← finsupp.range_total,
-  rw linear_map.mem_range,
-  apply mem_range_self l }
+  apply linear_equiv.of_bijective
+    (linear_map.cod_restrict (span R (range v)) (finsupp.total ι M R v) _),
+  { rw [← linear_map.ker_eq_bot, linear_map.ker_cod_restrict],
+    apply hv },
+  { rw [← linear_map.range_eq_top, linear_map.range_eq_map, linear_map.map_cod_restrict,
+      ← linear_map.range_le_iff_comap, range_subtype, map_top],
+    rw finsupp.range_total,
+    exact le_rfl },
+  { intro l,
+    rw ← finsupp.range_total,
+    rw linear_map.mem_range,
+    apply mem_range_self l }
 end
 
 /-- Linear combination representing a vector in the span of linearly independent vectors.
@@ -766,7 +767,8 @@ begin
     hv.repr x,
   { apply (linear_independent.total_equiv hv).injective,
     ext,
-    simp, },
+    simp only [linear_independent.total_equiv_apply_coe, equiv.self_comp_of_injective_symm,
+       linear_independent.total_repr, finsupp.total_equiv_map_domain, span.finsupp_total_repr], },
   ext ⟨_, ⟨i, rfl⟩⟩,
   simp [←p],
 end
@@ -850,7 +852,7 @@ begin
   rw [← finset.insert_erase hfi', finset.sum_insert (finset.not_mem_erase _ _),
       add_eq_zero_iff_eq_neg] at sum_f,
   rw sum_f,
-  refine neg_mem _ (sum_mem _ (λ c hc, smul_mem _ _ (subset_span ⟨c, _, rfl⟩))),
+  refine neg_mem (sum_mem (λ c hc, smul_mem _ _ (subset_span ⟨c, _, rfl⟩))),
   exact (memJ.mp (supp_f (finset.erase_subset _ _ hc))).resolve_left (finset.ne_of_mem_erase hc),
 end
 end repr
@@ -1082,7 +1084,7 @@ lemma linear_independent.insert (hs : linear_independent K (λ b, b : s → V))
   linear_independent K (λ b, b : insert x s → V) :=
 begin
   rw ← union_singleton,
-  have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem _) hx,
+  have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem (span K s)) hx,
   apply hs.union (linear_independent_singleton x0),
   rwa [disjoint_span_singleton' x0]
 end
diff --git a/src/linear_algebra/linear_pmap.lean b/src/linear_algebra/linear_pmap.lean
index c76b584f37e57..1219c832a44db 100644
--- a/src/linear_algebra/linear_pmap.lean
+++ b/src/linear_algebra/linear_pmap.lean
@@ -162,7 +162,7 @@ both `f` and `g` are defined at `x` and `f x = g x` form a submodule. -/
 def eq_locus (f g : linear_pmap R E F) : submodule R E :=
 { carrier   := {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), f ⟨x, hf⟩ = g ⟨x, hg⟩},
   zero_mem' := ⟨zero_mem _, zero_mem _, f.map_zero.trans g.map_zero.symm⟩,
-  add_mem'  := λ x y ⟨hfx, hgx, hx⟩ ⟨hfy, hgy, hy⟩, ⟨add_mem _ hfx hfy, add_mem _ hgx hgy,
+  add_mem'  := λ x y ⟨hfx, hgx, hx⟩ ⟨hfy, hgy, hy⟩, ⟨add_mem hfx hfy, add_mem hgx hgy,
     by erw [f.map_add ⟨x, hfx⟩ ⟨y, hfy⟩, g.map_add ⟨x, hgx⟩ ⟨y, hgy⟩, hx, hy]⟩,
   smul_mem' := λ c x ⟨hfx, hgx, hx⟩, ⟨smul_mem _ c hfx, smul_mem _ c hgx,
     by erw [f.map_smul c ⟨x, hfx⟩, g.map_smul c ⟨x, hgx⟩, hx]⟩ }
@@ -223,7 +223,8 @@ begin
     rw [add_comm, ← sub_eq_sub_iff_add_eq_add, eq_comm, ← map_sub, ← map_sub],
     apply h,
     simp only [← eq_sub_iff_add_eq] at hxy,
-    simp only [coe_sub, coe_mk, coe_mk, hxy, ← sub_add, ← sub_sub, sub_self, zero_sub, ← H],
+    simp only [add_subgroup_class.coe_sub, coe_mk, coe_mk, hxy, ← sub_add, ← sub_sub, sub_self,
+      zero_sub, ← H],
     apply neg_add_eq_sub },
   refine ⟨{ to_fun := fg, .. }, fg_eq⟩,
   { rintros ⟨z₁, hz₁⟩ ⟨z₂, hz₂⟩,
diff --git a/src/linear_algebra/prod.lean b/src/linear_algebra/prod.lean
index c3db935bebcae..9312be682ff39 100644
--- a/src/linear_algebra/prod.lean
+++ b/src/linear_algebra/prod.lean
@@ -459,12 +459,12 @@ begin
   split,
   { intros h,
     split,
-    { rintros _ ⟨x, hx, rfl⟩, apply h, exact ⟨hx, (zero_mem _)⟩, },
-    { rintros _ ⟨x, hx, rfl⟩, apply h, exact ⟨zero_mem _, hx⟩, }, },
+    { rintros _ ⟨x, hx, rfl⟩, apply h, exact ⟨hx, zero_mem p₂⟩, },
+    { rintros _ ⟨x, hx, rfl⟩, apply h, exact ⟨zero_mem p₁, hx⟩, }, },
   { rintros ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩,
     have h1' : (linear_map.inl R _ _) x1 ∈ q, { apply hH, simpa using h1, },
     have h2' : (linear_map.inr R _ _) x2 ∈ q, { apply hK, simpa using h2, },
-    simpa using add_mem _ h1' h2', }
+    simpa using add_mem h1' h2', }
 end
 
 lemma prod_eq_bot_iff {p₁ : submodule R M} {p₂ : submodule R M₂} :
diff --git a/src/linear_algebra/quotient.lean b/src/linear_algebra/quotient.lean
index 990baf46697da..feaeb98a38221 100644
--- a/src/linear_algebra/quotient.lean
+++ b/src/linear_algebra/quotient.lean
@@ -27,8 +27,8 @@ open linear_map
 /-- The equivalence relation associated to a submodule `p`, defined by `x ≈ y` iff `y - x ∈ p`. -/
 def quotient_rel : setoid M :=
 ⟨λ x y, x - y ∈ p, λ x, by simp,
- λ x y h, by simpa using neg_mem _ h,
- λ x y z h₁ h₂, by simpa [sub_eq_add_neg, add_left_comm, add_assoc] using add_mem _ h₁ h₂⟩
+ λ x y h, by simpa using neg_mem h,
+ λ x y z h₁ h₂, by simpa [sub_eq_add_neg, add_left_comm, add_assoc] using add_mem h₁ h₂⟩
 
 /-- The quotient of a module `M` by a submodule `p ⊆ M`. -/
 instance has_quotient : has_quotient M (submodule R M) := ⟨λ p, quotient (quotient_rel p)⟩
@@ -57,20 +57,20 @@ by simpa using (quotient.eq p : mk x = 0 ↔ _)
 instance : has_add (M ⧸ p) :=
 ⟨λ a b, quotient.lift_on₂' a b (λ a b, mk (a + b)) $
   λ a₁ a₂ b₁ b₂ h₁ h₂, (quotient.eq p).2 $
-    by simpa [sub_eq_add_neg, add_left_comm, add_comm] using add_mem p h₁ h₂⟩
+    by simpa [sub_eq_add_neg, add_left_comm, add_comm] using add_mem h₁ h₂⟩
 
 @[simp] theorem mk_add : (mk (x + y) : M ⧸ p) = mk x + mk y := rfl
 
 instance : has_neg (M ⧸ p) :=
 ⟨λ a, quotient.lift_on' a (λ a, mk (-a)) $
- λ a b h, (quotient.eq p).2 $ by simpa using neg_mem p h⟩
+ λ a b h, (quotient.eq p).2 $ by simpa using neg_mem h⟩
 
 @[simp] theorem mk_neg : (mk (-x) : M ⧸ p) = -mk x := rfl
 
 instance : has_sub (M ⧸ p) :=
 ⟨λ a b, quotient.lift_on₂' a b (λ a b, mk (a - b)) $
   λ a₁ a₂ b₁ b₂ h₁ h₂, (quotient.eq p).2 $
-  by simpa [sub_eq_add_neg, add_left_comm, add_comm] using add_mem p h₁ (neg_mem p h₂)⟩
+  by simpa [sub_eq_add_neg, add_left_comm, add_comm] using add_mem h₁ (neg_mem h₂)⟩
 
 @[simp] theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y := rfl
 
diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean
index fa379faf22a81..b3e27235d2fb1 100644
--- a/src/linear_algebra/span.lean
+++ b/src/linear_algebra/span.lean
@@ -113,7 +113,7 @@ begin
   refine exists.elim _ (λ (hx : x ∈ span R s) (hc : p x hx), hc),
   refine span_induction hx (λ m hm, ⟨subset_span hm, Hs m hm⟩) ⟨zero_mem _, H0⟩
     (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
-    ⟨add_mem _ hx' hy', H1 _ _ _ _ hx hy⟩) (λ r x hx, exists.elim hx $ λ hx' hx,
+    ⟨add_mem hx' hy', H1 _ _ _ _ hx hy⟩) (λ r x hx, exists.elim hx $ λ hx' hx,
     ⟨smul_mem _ _ hx', H2 r _ _ hx⟩)
 end
 
@@ -122,7 +122,7 @@ eq_top_iff.2 $ λ x, subtype.rec_on x $ λ x hx _, begin
   refine span_induction' (λ x hx, _) _ (λ x y _ _, _) (λ r x _, _) hx,
   { exact subset_span hx },
   { exact zero_mem _ },
-  { exact add_mem _ },
+  { exact add_mem },
   { exact smul_mem _ _ }
 end
 
@@ -227,7 +227,7 @@ begin
   { exact hι.elim (λ i, ⟨i, (S i).zero_mem⟩) },
   { intros x y i hi j hj,
     rcases H i j with ⟨k, ik, jk⟩,
-    exact ⟨k, add_mem _ (ik hi) (jk hj)⟩ },
+    exact ⟨k, add_mem (ik hi) (jk hj)⟩ },
   { exact λ a x i hi, ⟨i, smul_mem _ a hi⟩ },
 end
 
@@ -271,11 +271,11 @@ lemma mem_sup : x ∈ p ⊔ p' ↔ ∃ (y ∈ p) (z ∈ p'), y + z = x :=
     { exact ⟨0, by simp, y, h, by simp⟩ } },
   { exact ⟨0, by simp, 0, by simp⟩ },
   { rintro _ _ ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩,
-    exact ⟨_, add_mem _ hy₁ hy₂, _, add_mem _ hz₁ hz₂, by simp [add_assoc]; cc⟩ },
+    exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by simp [add_assoc]; cc⟩ },
   { rintro a _ ⟨y, hy, z, hz, rfl⟩,
     exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩ }
 end,
-by rintro ⟨y, hy, z, hz, rfl⟩; exact add_mem _
+by rintro ⟨y, hy, z, hz, rfl⟩; exact add_mem
   ((le_sup_left : p ≤ p ⊔ p') hy)
   ((le_sup_right : p' ≤ p ⊔ p') hz)⟩
 
@@ -533,7 +533,7 @@ end
 lemma supr_induction' {ι : Sort*} (p : ι → submodule R M) {C : Π x, (x ∈ ⨆ i, p i) → Prop}
   (hp : ∀ i (x ∈ p i), C x (mem_supr_of_mem i ‹_›))
   (h0 : C 0 (zero_mem _))
-  (hadd : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem _ ‹_› ‹_›))
+  (hadd : ∀ x y hx hy, C x hx → C y hy → C (x + y) (add_mem ‹_› ‹_›))
   {x : M} (hx : x ∈ ⨆ i, p i) : C x hx :=
 begin
   refine exists.elim _ (λ (hx : x ∈ ⨆ i, p i) (hc : C x hx), hc),
diff --git a/src/linear_algebra/std_basis.lean b/src/linear_algebra/std_basis.lean
index 36775db5667f4..1092e00ed8a6e 100644
--- a/src/linear_algebra/std_basis.lean
+++ b/src/linear_algebra/std_basis.lean
@@ -101,7 +101,7 @@ begin
     assume hiI,
     rw [std_basis_same],
     exact hb _ ((hu trivial).resolve_left hiI) },
-  exact sum_mem _ (assume i hiI, mem_supr_of_mem i $ mem_supr_of_mem hiI $
+  exact sum_mem (assume i hiI, mem_supr_of_mem i $ mem_supr_of_mem hiI $
     (std_basis R φ i).mem_range_self (b i))
 end
 
diff --git a/src/ring_theory/adjoin/fg.lean b/src/ring_theory/adjoin/fg.lean
index 76874cf160f36..8765ea074d400 100644
--- a/src/ring_theory/adjoin/fg.lean
+++ b/src/ring_theory/adjoin/fg.lean
@@ -58,7 +58,7 @@ begin
     rcases hr with ⟨l, hlq, rfl⟩,
     have := @finsupp.total_apply A A (adjoin R s),
     rw [this, finsupp.sum],
-    refine sum_mem _ _,
+    refine sum_mem _,
     intros z hz, change (l z).1 * _ ∈ _,
     have : (l z).1 ∈ (adjoin R s).to_submodule := (l z).2,
     rw [← hp', ← set.image_id p, finsupp.mem_span_image_iff_total R] at this,
@@ -66,7 +66,7 @@ begin
     have := @finsupp.total_apply A A R,
     rw this at hl,
     rw [←hl, finsupp.sum_mul],
-    refine sum_mem _ _,
+    refine sum_mem _,
     intros t ht, change _ * _ ∈ _, rw smul_mul_assoc, refine smul_mem _ _ _,
     exact subset_span ⟨t, z, hlp ht, hlq hz, rfl⟩ }
 end
diff --git a/src/ring_theory/algebra_tower.lean b/src/ring_theory/algebra_tower.lean
index 41686bb7dd95c..31c0841cb6f67 100644
--- a/src/ring_theory/algebra_tower.lean
+++ b/src/ring_theory/algebra_tower.lean
@@ -243,7 +243,7 @@ begin
     from mem_image_of_mem _ $ mem_product.2 ⟨mem_union_right _ $ finset.mul_mem_mul hyi hyj, hyk⟩,
   have hxy : ∀ xi ∈ x, xi ∈ span (algebra.adjoin A (↑s : set B))
                (↑(insert 1 y : finset C) : set C) :=
-    λ xi hxi, hf xi ▸ sum_mem _ (λ yj hyj, smul_mem
+    λ xi hxi, hf xi ▸ sum_mem (λ yj hyj, smul_mem
       (span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C))
       ⟨f xi yj, algebra.subset_adjoin $ hsx xi hxi yj hyj⟩
       (subset_span $ mem_insert_of_mem hyj)),
@@ -254,7 +254,7 @@ begin
     { rw mul_one, exact subset_span (set.mem_insert _ _) },
     { rw one_mul, exact subset_span (set.mem_insert_of_mem _ hyj) },
     { rw mul_one, exact subset_span (set.mem_insert_of_mem _ hyi) },
-    { rw ← hf (yi * yj), exact set_like.mem_coe.2 (sum_mem _ $ λ yk hyk, smul_mem
+    { rw ← hf (yi * yj), exact set_like.mem_coe.2 (sum_mem $ λ yk hyk, smul_mem
         (span (algebra.adjoin A (↑s : set B)) (insert 1 ↑y : set C))
         ⟨f (yi * yj) yk, algebra.subset_adjoin $ hsy yi hyi yj hyj yk hyk⟩
         (subset_span $ set.mem_insert_of_mem _ hyk : yk ∈ _)) } },
diff --git a/src/ring_theory/graded_algebra/homogeneous_localization.lean b/src/ring_theory/graded_algebra/homogeneous_localization.lean
index 9a529f2123b17..d10416d0e37a3 100644
--- a/src/ring_theory/graded_algebra/homogeneous_localization.lean
+++ b/src/ring_theory/graded_algebra/homogeneous_localization.lean
@@ -139,7 +139,7 @@ instance : has_add (num_denom_same_deg 𝒜 x) :=
 { add := λ c1 c2,
   { deg := c1.deg + c2.deg,
     num := ⟨c1.denom * c2.num + c2.denom * c1.num,
-      add_mem _ (mul_mem c1.denom.2 c2.num.2)
+      add_mem (mul_mem c1.denom.2 c2.num.2)
         (add_comm c2.deg c1.deg ▸ mul_mem c2.denom.2 c1.num.2)⟩,
     denom := ⟨c1.denom * c2.denom, mul_mem c1.denom.2 c2.denom.2⟩,
     denom_not_mem := λ r, or.elim
@@ -152,7 +152,7 @@ instance : has_add (num_denom_same_deg 𝒜 x) :=
   ((c1 + c2).denom : A) = c1.denom * c2.denom := rfl
 
 instance : has_neg (num_denom_same_deg 𝒜 x) :=
-{ neg := λ c, ⟨c.deg, ⟨-c.num, neg_mem _ c.num.2⟩, c.denom, c.denom_not_mem⟩ }
+{ neg := λ c, ⟨c.deg, ⟨-c.num, neg_mem c.num.2⟩, c.denom, c.denom_not_mem⟩ }
 
 @[simp] lemma deg_neg (c : num_denom_same_deg 𝒜 x) : (-c).deg = c.deg := rfl
 @[simp] lemma num_neg (c : num_denom_same_deg 𝒜 x) : ((-c).num : A) = -c.num := rfl
diff --git a/src/ring_theory/ideal/basic.lean b/src/ring_theory/ideal/basic.lean
index 0beb985e3f329..64a34e625a2cf 100644
--- a/src/ring_theory/ideal/basic.lean
+++ b/src/ring_theory/ideal/basic.lean
@@ -469,13 +469,10 @@ namespace ideal
 
 variables [ring α] (I : ideal α) {a b : α}
 
-lemma neg_mem_iff : -a ∈ I ↔ a ∈ I := I.neg_mem_iff
-
-lemma add_mem_iff_left : b ∈ I → (a + b ∈ I ↔ a ∈ I) := I.add_mem_iff_left
-
-lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right
-
-protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := I.sub_mem
+protected lemma neg_mem_iff : -a ∈ I ↔ a ∈ I := neg_mem_iff
+protected lemma add_mem_iff_left : b ∈ I → (a + b ∈ I ↔ a ∈ I) := I.add_mem_iff_left
+protected lemma add_mem_iff_right : a ∈ I → (a + b ∈ I ↔ b ∈ I) := I.add_mem_iff_right
+protected lemma sub_mem : a ∈ I → b ∈ I → a - b ∈ I := sub_mem
 
 lemma mem_span_insert' {s : set α} {x y} :
   x ∈ span (insert y s) ↔ ∃a, x + a * y ∈ span s := submodule.mem_span_insert'
diff --git a/src/ring_theory/integral_closure.lean b/src/ring_theory/integral_closure.lean
index aacfb83b4663e..f6f066cff1e7d 100644
--- a/src/ring_theory/integral_closure.lean
+++ b/src/ring_theory/integral_closure.lean
@@ -178,7 +178,7 @@ begin
   have : degree (p %ₘ f) ≤ degree f := degree_mod_by_monic_le p hfm,
   generalize_hyp : p %ₘ f = q at this ⊢,
   rw [← sum_C_mul_X_eq q, aeval_def, eval₂_sum, sum_def],
-  refine sum_mem _ (λ k hkq, _),
+  refine sum_mem (λ k hkq, _),
   rw [eval₂_mul, eval₂_C, eval₂_pow, eval₂_X, ← algebra.smul_def],
   refine smul_mem _ _ (subset_span _),
   rw finset.mem_coe, refine finset.mem_image.2 ⟨_, _, rfl⟩,
@@ -228,7 +228,7 @@ begin
     subring.closure ↑(lx.frange ∪ finset.bUnion finset.univ (finsupp.frange ∘ ly)),
   -- It suffices to prove that `x` is integral over `S₀`.
   refine is_integral_of_subring S₀ _,
-  letI : comm_ring S₀ := subring.to_comm_ring S₀,
+  letI : comm_ring S₀ := subring_class.to_comm_ring S₀,
   letI : algebra S₀ A := algebra.of_subring S₀,
   -- Claim: the `S₀`-module span (in `A`) of the set `y ∪ {1}` is closed under
   -- multiplication (indeed, this is the motivation for the definition of `S₀`).
diff --git a/src/ring_theory/jacobson_ideal.lean b/src/ring_theory/jacobson_ideal.lean
index da4cc470d7b99..e8eb9f9819f39 100644
--- a/src/ring_theory/jacobson_ideal.lean
+++ b/src/ring_theory/jacobson_ideal.lean
@@ -104,7 +104,7 @@ theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, x * y * z
         ← neg_sub, neg_mul, neg_mul_eq_mul_neg, mul_comm x y, mul_comm _ (- z)],
       rcases hy with ⟨i, hi, df⟩,
       rw [← (sub_eq_iff_eq_add.mpr df.symm), sub_sub, add_comm, ← sub_sub, sub_self, zero_sub],
-      refine M.mul_mem_left (-z) ((neg_mem_iff _).mpr hi) }) (him hz)⟩
+      refine M.mul_mem_left (-z) (neg_mem_iff.mpr hi) }) (him hz)⟩
 
 lemma exists_mul_sub_mem_of_sub_one_mem_jacobson {I : ideal R} (r : R)
   (h : r - 1 ∈ jacobson I) : ∃ s, r * s - 1 ∈ I :=
diff --git a/src/ring_theory/local_properties.lean b/src/ring_theory/local_properties.lean
index 8f584a4e70ad9..55d84571f12df 100644
--- a/src/ring_theory/local_properties.lean
+++ b/src/ring_theory/local_properties.lean
@@ -484,7 +484,7 @@ begin
     (submonoid.map (algebra_map R S : R →* S) M) s : set S)).smul_mem hx' a using 1,
   convert ha₂.symm,
   { rw [mul_comm (y' ^ n • x), subtype.coe_mk, submonoid.smul_def, submonoid.coe_mul, ← smul_smul,
-    algebra.smul_def, submonoid.coe_pow], refl },
+        algebra.smul_def, submonoid_class.coe_pow], refl },
   { rw mul_comm, exact algebra.smul_def _ _ }
 end
 
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 58a351b09d5ba..c0055a5c30835 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -132,7 +132,7 @@ begin
     rw mem_smul_span_singleton at hy, rcases hy with ⟨d, hdi, rfl⟩,
     change _ • _ ∈ I • span R s,
     rw [mul_smul, ← hyz, smul_add, smul_smul, mul_comm, mul_smul],
-    exact add_mem _ (smul_mem _ _ hci) (smul_mem _ _ hz) }
+    exact add_mem (smul_mem _ _ hci) (smul_mem _ _ hz) }
 end
 
 theorem fg_bot : (⊥ : submodule R M).fg :=
diff --git a/src/ring_theory/polynomial/scale_roots.lean b/src/ring_theory/polynomial/scale_roots.lean
index a365df87f4817..5c7d9c18bed7c 100644
--- a/src/ring_theory/polynomial/scale_roots.lean
+++ b/src/ring_theory/polynomial/scale_roots.lean
@@ -58,7 +58,7 @@ le_antisymm (support_scale_roots_le p s)
     intro i,
     simp only [coeff_scale_roots, polynomial.mem_support_iff],
     intros p_ne_zero ps_zero,
-    have := ((non_zero_divisors R).pow_mem hs (p.nat_degree - i)) _ ps_zero,
+    have := pow_mem hs (p.nat_degree - i) _ ps_zero,
     contradiction
   end
 
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
index 674287b306638..4aeb34fc49dc6 100644
--- a/src/ring_theory/principal_ideal_domain.lean
+++ b/src/ring_theory/principal_ideal_domain.lean
@@ -240,7 +240,7 @@ lemma mem_submonoid_of_factors_subset_of_units_subset (s : submonoid R)
 begin
   rcases ((factors_spec a ha).2) with ⟨c, hc⟩,
   rw [← hc],
-  exact submonoid.mul_mem _ (submonoid.multiset_prod_mem _ _ hfac) (hunit _),
+  exact mul_mem (multiset_prod_mem _ hfac) (hunit _)
 end
 
 /-- If a `ring_hom` maps all units and all factors of an element `a` into a submonoid `s`, then it
diff --git a/src/ring_theory/subring/basic.lean b/src/ring_theory/subring/basic.lean
index 713b374242ad7..57554df96a9d1 100644
--- a/src/ring_theory/subring/basic.lean
+++ b/src/ring_theory/subring/basic.lean
@@ -83,13 +83,11 @@ instance subring_class.add_subgroup_class (S : Type*) (R : out_param $ Type u) [
 variables [set_like S R] [hSR : subring_class S R] (s : S)
 include hSR
 
-namespace subring_class
-
-open one_mem_class add_subgroup_class
-
 lemma coe_int_mem (n : ℤ) : (n : R) ∈ s :=
 by simp only [← zsmul_one, zsmul_mem, one_mem]
 
+namespace subring_class
+
 /-- A subring of a ring inherits a ring structure -/
 @[priority 75] -- Prefer subclasses of `ring` over subclasses of `subring_class`.
 instance to_ring : ring s :=
@@ -295,64 +293,53 @@ namespace subring
 variables (s : subring R)
 
 /-- A subring contains the ring's 1. -/
-theorem one_mem : (1 : R) ∈ s := s.one_mem'
+protected theorem one_mem : (1 : R) ∈ s := one_mem _
 
 /-- A subring contains the ring's 0. -/
-theorem zero_mem : (0 : R) ∈ s := s.zero_mem'
+protected theorem zero_mem : (0 : R) ∈ s := zero_mem _
 
 /-- A subring is closed under multiplication. -/
-theorem mul_mem : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s := s.mul_mem'
+protected theorem mul_mem {x y : R} : x ∈ s → y ∈ s → x * y ∈ s := mul_mem
 
 /-- A subring is closed under addition. -/
-theorem add_mem : ∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s := s.add_mem'
+protected theorem add_mem {x y : R} : x ∈ s → y ∈ s → x + y ∈ s := add_mem
 
 /-- A subring is closed under negation. -/
-theorem neg_mem : ∀ {x : R}, x ∈ s → -x ∈ s := s.neg_mem'
+protected theorem neg_mem {x : R} : x ∈ s → -x ∈ s := neg_mem
 
 /-- A subring is closed under subtraction -/
-theorem sub_mem {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s :=
-by { rw sub_eq_add_neg, exact s.add_mem hx (s.neg_mem hy) }
+protected theorem sub_mem {x y : R} (hx : x ∈ s) (hy : y ∈ s) : x - y ∈ s := sub_mem hx hy
 
 /-- Product of a list of elements in a subring is in the subring. -/
-lemma list_prod_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.prod ∈ s :=
-s.to_submonoid.list_prod_mem
+protected lemma list_prod_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.prod ∈ s := list_prod_mem
 
 /-- Sum of a list of elements in a subring is in the subring. -/
-lemma list_sum_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.sum ∈ s :=
-s.to_add_subgroup.list_sum_mem
+protected lemma list_sum_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.sum ∈ s := list_sum_mem
 
 /-- Product of a multiset of elements in a subring of a `comm_ring` is in the subring. -/
-lemma multiset_prod_mem {R} [comm_ring R] (s : subring R) (m : multiset R) :
+protected lemma multiset_prod_mem {R} [comm_ring R] (s : subring R) (m : multiset R) :
   (∀a ∈ m, a ∈ s) → m.prod ∈ s :=
-s.to_submonoid.multiset_prod_mem m
+multiset_prod_mem _
 
 /-- Sum of a multiset of elements in an `subring` of a `ring` is
 in the `subring`. -/
-lemma multiset_sum_mem {R} [ring R] (s : subring R) (m : multiset R) :
+protected lemma multiset_sum_mem {R} [ring R] (s : subring R) (m : multiset R) :
   (∀a ∈ m, a ∈ s) → m.sum ∈ s :=
-s.to_add_subgroup.multiset_sum_mem m
+multiset_sum_mem _
 
 /-- Product of elements of a subring of a `comm_ring` indexed by a `finset` is in the
     subring. -/
-lemma prod_mem {R : Type*} [comm_ring R] (s : subring R)
+protected lemma prod_mem {R : Type*} [comm_ring R] (s : subring R)
   {ι : Type*} {t : finset ι} {f : ι → R} (h : ∀c ∈ t, f c ∈ s) :
   ∏ i in t, f i ∈ s :=
-s.to_submonoid.prod_mem h
+prod_mem h
 
 /-- Sum of elements in a `subring` of a `ring` indexed by a `finset`
 is in the `subring`. -/
-lemma sum_mem {R : Type*} [ring R] (s : subring R)
+protected lemma sum_mem {R : Type*} [ring R] (s : subring R)
   {ι : Type*} {t : finset ι} {f : ι → R} (h : ∀c ∈ t, f c ∈ s) :
   ∑ i in t, f i ∈ s :=
-s.to_add_subgroup.sum_mem h
-
-lemma pow_mem {x : R} (hx : x ∈ s) (n : ℕ) : x^n ∈ s := s.to_submonoid.pow_mem hx n
-
-lemma zsmul_mem {x : R} (hx : x ∈ s) (n : ℤ) :
-  n • x ∈ s := s.to_add_subgroup.zsmul_mem hx n
-
-lemma coe_int_mem (n : ℤ) : (n : R) ∈ s :=
-by simp only [← zsmul_one, zsmul_mem, one_mem]
+sum_mem h
 
 /-- A subring of a ring inherits a ring structure -/
 instance to_ring : ring s :=
@@ -360,13 +347,19 @@ instance to_ring : ring s :=
   left_distrib := λ x y z, subtype.eq $ left_distrib x y z,
   .. s.to_submonoid.to_monoid, .. s.to_add_subgroup.to_add_comm_group }
 
+protected lemma zsmul_mem {x : R} (hx : x ∈ s) (n : ℤ) : n • x ∈ s := zsmul_mem hx n
+
+protected lemma pow_mem {x : R} (hx : x ∈ s) (n : ℕ) : x^n ∈ s := pow_mem hx n
+
 @[simp, norm_cast] lemma coe_add (x y : s) : (↑(x + y) : R) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_neg (x : s) : (↑(-x) : R) = -↑x := rfl
 @[simp, norm_cast] lemma coe_mul (x y : s) : (↑(x * y) : R) = ↑x * ↑y := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : s) : R) = 0 := rfl
 @[simp, norm_cast] lemma coe_one : ((1 : s) : R) = 1 := rfl
-@[simp, norm_cast] lemma coe_pow (x : s) (n : ℕ) : (↑(x ^ n) : R) = x ^ n := rfl
+@[simp, norm_cast] lemma coe_pow (x : s) (n : ℕ) : (↑(x ^ n) : R) = x ^ n :=
+submonoid_class.coe_pow x n
 
+-- TODO: can be generalized to `add_submonoid_class`
 @[simp] lemma coe_eq_zero_iff {x : s} : (x : R) = 0 ↔ x = 0 :=
 ⟨λ h, subtype.ext (trans h s.coe_zero.symm),
  λ h, h.symm ▸ s.coe_zero⟩
@@ -583,7 +576,7 @@ lemma mem_Inf {S : set (subring R)} {x : R} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈
 /-- Subrings of a ring form a complete lattice. -/
 instance : complete_lattice (subring R) :=
 { bot := (⊥),
-  bot_le := λ s x hx, let ⟨n, hn⟩ := mem_bot.1 hx in hn ▸ s.coe_int_mem n,
+  bot_le := λ s x hx, let ⟨n, hn⟩ := mem_bot.1 hx in hn ▸ coe_int_mem s n,
   top := (⊤),
   le_top := λ s x hx, trivial,
   inf := (⊓),
@@ -717,30 +710,30 @@ end
 
 lemma mem_closure_iff {s : set R} {x} :
   x ∈ closure s ↔ x ∈ add_subgroup.closure (submonoid.closure s : set R) :=
-⟨ λ h, closure_induction h (λ x hx, add_subgroup.subset_closure $ submonoid.subset_closure hx )
+⟨λ h, closure_induction h (λ x hx, add_subgroup.subset_closure $ submonoid.subset_closure hx)
  (add_subgroup.zero_mem _)
  (add_subgroup.subset_closure ( submonoid.one_mem (submonoid.closure s)) )
  (λ x y hx hy, add_subgroup.add_mem _ hx hy )
  (λ x hx, add_subgroup.neg_mem _ hx )
- ( λ x y hx hy, add_subgroup.closure_induction hy
-  (λ q hq, add_subgroup.closure_induction hx
-    ( λ p hp, add_subgroup.subset_closure ((submonoid.closure s).mul_mem hp hq) )
-    ( begin rw zero_mul q, apply add_subgroup.zero_mem _, end )
-    ( λ p₁ p₂ ihp₁ ihp₂, begin rw add_mul p₁ p₂ q, apply add_subgroup.add_mem _ ihp₁ ihp₂, end )
-    ( λ x hx, begin have f : -x * q = -(x*q) :=
-      by simp, rw f, apply add_subgroup.neg_mem _ hx, end ) )
-  ( begin rw mul_zero x, apply add_subgroup.zero_mem _, end )
-  ( λ q₁ q₂ ihq₁ ihq₂, begin rw mul_add x q₁ q₂, apply add_subgroup.add_mem _ ihq₁ ihq₂ end )
-  ( λ z hz, begin have f : x * -z = -(x*z) := by simp,
-            rw f, apply add_subgroup.neg_mem _ hz, end ) ),
+   (λ x y hx hy, add_subgroup.closure_induction hy
+     (λ q hq, add_subgroup.closure_induction hx
+       (λ p hp, add_subgroup.subset_closure ((submonoid.closure s).mul_mem hp hq))
+       (begin rw zero_mul q, apply add_subgroup.zero_mem _, end)
+       (λ p₁ p₂ ihp₁ ihp₂, begin rw add_mul p₁ p₂ q, apply add_subgroup.add_mem _ ihp₁ ihp₂, end)
+       (λ x hx, begin have f : -x * q = -(x*q) :=
+         by simp, rw f, apply add_subgroup.neg_mem _ hx, end))
+     (begin rw mul_zero x, apply add_subgroup.zero_mem _, end)
+     (λ q₁ q₂ ihq₁ ihq₂, begin rw mul_add x q₁ q₂, apply add_subgroup.add_mem _ ihq₁ ihq₂ end)
+     (λ z hz, begin have f : x * -z = -(x*z) := by simp,
+       rw f, apply add_subgroup.neg_mem _ hz, end)),
  λ h, add_subgroup.closure_induction h
- ( λ x hx, submonoid.closure_induction hx
-  ( λ x hx, subset_closure hx )
-  ( one_mem _ )
-  ( λ x y hx hy, mul_mem _ hx hy ) )
- ( zero_mem _ )
- (λ x y hx hy, add_mem _ hx hy)
- ( λ x hx, neg_mem _ hx ) ⟩
+   (λ x hx, submonoid.closure_induction hx
+     (λ x hx, subset_closure hx)
+     (one_mem _)
+     (λ x y hx hy, mul_mem hx hy))
+ (zero_mem _)
+ (λ x y hx hy, add_mem hx hy)
+ (λ x hx, neg_mem hx)⟩
 
 /-- If all elements of `s : set A` commute pairwise, then `closure s` is a commutative ring.  -/
 def closure_comm_ring_of_comm {s : set R} (hcomm : ∀ (a ∈ s) (b ∈ s), a * b = b * a) :
@@ -996,7 +989,7 @@ lemma range_snd : (snd R S).srange = ⊤ :=
 lemma prod_bot_sup_bot_prod (s : subring R) (t : subring S) :
   (s.prod ⊥) ⊔ (prod ⊥ t) = s.prod t :=
 le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) $
-assume p hp, prod.fst_mul_snd p ▸ mul_mem _
+assume p hp, prod.fst_mul_snd p ▸ mul_mem
   ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, set_like.mem_coe.2 $ one_mem ⊥⟩)
   ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨set_like.mem_coe.2 $ one_mem ⊥, hp.2⟩)
 
@@ -1090,7 +1083,6 @@ lemma add_subgroup.int_mul_mem {G : add_subgroup R} (k : ℤ) {g : R} (h : g ∈
   (k : R) * g ∈ G :=
 by { convert add_subgroup.zsmul_mem G h k, simp }
 
-
 /-! ## Actions by `subring`s
 
 These are just copies of the definitions about `subsemiring` starting from
diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
index a002c626b47f5..2812504064041 100644
--- a/src/ring_theory/subsemiring/basic.lean
+++ b/src/ring_theory/subsemiring/basic.lean
@@ -43,13 +43,11 @@ instance subsemiring_class.add_submonoid_class (S : Type*) (R : out_param $ Type
 variables [set_like S R] [hSR : subsemiring_class S R] (s : S)
 include hSR
 
-open one_mem_class add_submonoid_class
-
-namespace subsemiring_class
-
 lemma coe_nat_mem (n : ℕ) : (n : R) ∈ s :=
 by simp only [← nsmul_one, nsmul_mem, one_mem]
 
+namespace subsemiring_class
+
 /-- A subsemiring of a `non_assoc_semiring` inherits a `non_assoc_semiring` structure -/
 @[priority 75] -- Prefer subclasses of `non_assoc_semiring` over subclasses of `subsemiring_class`.
 instance to_non_assoc_semiring : non_assoc_semiring s :=
@@ -216,61 +214,50 @@ namespace subsemiring
 variables (s : subsemiring R)
 
 /-- A subsemiring contains the semiring's 1. -/
-theorem one_mem : (1 : R) ∈ s := s.one_mem'
+protected theorem one_mem : (1 : R) ∈ s := one_mem s
 
 /-- A subsemiring contains the semiring's 0. -/
-theorem zero_mem : (0 : R) ∈ s := s.zero_mem'
+protected theorem zero_mem : (0 : R) ∈ s := zero_mem s
 
 /-- A subsemiring is closed under multiplication. -/
-theorem mul_mem : ∀ {x y : R}, x ∈ s → y ∈ s → x * y ∈ s := s.mul_mem'
+protected theorem mul_mem {x y : R} : x ∈ s → y ∈ s → x * y ∈ s := mul_mem
 
 /-- A subsemiring is closed under addition. -/
-theorem add_mem : ∀ {x y : R}, x ∈ s → y ∈ s → x + y ∈ s := s.add_mem'
+protected theorem add_mem {x y : R} : x ∈ s → y ∈ s → x + y ∈ s := add_mem
 
 /-- Product of a list of elements in a `subsemiring` is in the `subsemiring`. -/
 lemma list_prod_mem {R : Type*} [semiring R] (s : subsemiring R) {l : list R} :
   (∀x ∈ l, x ∈ s) → l.prod ∈ s :=
-s.to_submonoid.list_prod_mem
+list_prod_mem
 
 /-- Sum of a list of elements in a `subsemiring` is in the `subsemiring`. -/
-lemma list_sum_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.sum ∈ s :=
-s.to_add_submonoid.list_sum_mem
+protected lemma list_sum_mem {l : list R} : (∀x ∈ l, x ∈ s) → l.sum ∈ s := list_sum_mem
 
 /-- Product of a multiset of elements in a `subsemiring` of a `comm_semiring`
     is in the `subsemiring`. -/
-lemma multiset_prod_mem {R} [comm_semiring R] (s : subsemiring R) (m : multiset R) :
+protected lemma multiset_prod_mem {R} [comm_semiring R] (s : subsemiring R) (m : multiset R) :
   (∀a ∈ m, a ∈ s) → m.prod ∈ s :=
-s.to_submonoid.multiset_prod_mem m
+multiset_prod_mem m
 
 /-- Sum of a multiset of elements in a `subsemiring` of a `semiring` is
 in the `add_subsemiring`. -/
-lemma multiset_sum_mem (m : multiset R) :
+protected lemma multiset_sum_mem (m : multiset R) :
   (∀a ∈ m, a ∈ s) → m.sum ∈ s :=
-s.to_add_submonoid.multiset_sum_mem m
+multiset_sum_mem m
 
 /-- Product of elements of a subsemiring of a `comm_semiring` indexed by a `finset` is in the
     subsemiring. -/
-lemma prod_mem {R : Type*} [comm_semiring R] (s : subsemiring R)
+protected lemma prod_mem {R : Type*} [comm_semiring R] (s : subsemiring R)
   {ι : Type*} {t : finset ι} {f : ι → R} (h : ∀c ∈ t, f c ∈ s) :
   ∏ i in t, f i ∈ s :=
-s.to_submonoid.prod_mem h
+prod_mem h
 
 /-- Sum of elements in an `subsemiring` of an `semiring` indexed by a `finset`
 is in the `add_subsemiring`. -/
-lemma sum_mem (s : subsemiring R)
+protected lemma sum_mem (s : subsemiring R)
   {ι : Type*} {t : finset ι} {f : ι → R} (h : ∀c ∈ t, f c ∈ s) :
   ∑ i in t, f i ∈ s :=
-s.to_add_submonoid.sum_mem h
-
-lemma pow_mem {R : Type*} [semiring R] (s : subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) :
-  x^n ∈ s := s.to_submonoid.pow_mem hx n
-
-lemma nsmul_mem {x : R} (hx : x ∈ s) (n : ℕ) :
-  n • x ∈ s := s.to_add_submonoid.nsmul_mem hx n
-
-lemma coe_nat_mem (n : ℕ) : (n : R) ∈ s :=
-by simp only [← nsmul_one, nsmul_mem, one_mem]
-
+sum_mem h
 /-- A subsemiring of a `non_assoc_semiring` inherits a `non_assoc_semiring` structure -/
 instance to_non_assoc_semiring : non_assoc_semiring s :=
 { mul_zero := λ x, subtype.eq $ mul_zero x,
@@ -287,6 +274,9 @@ instance to_non_assoc_semiring : non_assoc_semiring s :=
 instance nontrivial [nontrivial R] : nontrivial s :=
 nontrivial_of_ne 0 1 $ λ H, zero_ne_one (congr_arg subtype.val H)
 
+protected lemma pow_mem {R : Type*} [semiring R] (s : subsemiring R) {x : R} (hx : x ∈ s) (n : ℕ) :
+  x^n ∈ s := pow_mem hx n
+
 instance no_zero_divisors [no_zero_divisors R] : no_zero_divisors s :=
 { eq_zero_or_eq_zero_of_mul_eq_zero := λ x y h,
   or.cases_on (eq_zero_or_eq_zero_of_mul_eq_zero $ subtype.ext_iff.mp h)
@@ -333,6 +323,8 @@ subtype.coe_injective.linear_ordered_semiring coe
 
 /-! Note: currently, there is no `linear_ordered_comm_semiring`. -/
 
+protected lemma nsmul_mem {x : R} (hx : x ∈ s) (n : ℕ) :
+  n • x ∈ s := nsmul_mem hx n
 
 @[simp] lemma mem_to_submonoid {s : subsemiring R} {x : R} : x ∈ s.to_submonoid ↔ x ∈ s := iff.rfl
 @[simp] lemma coe_to_submonoid (s : subsemiring R) : (s.to_submonoid : set R) = s := rfl
@@ -471,7 +463,7 @@ mk'_to_add_submonoid _ _
 /-- Subsemirings of a semiring form a complete lattice. -/
 instance : complete_lattice (subsemiring R) :=
 { bot := (⊥),
-  bot_le := λ s x hx, let ⟨n, hn⟩ := mem_bot.1 hx in hn ▸ s.coe_nat_mem n,
+  bot_le := λ s x hx, let ⟨n, hn⟩ := mem_bot.1 hx in hn ▸ coe_nat_mem s n,
   top := (⊤),
   le_top := λ s x hx, trivial,
   inf := (⊓),
@@ -685,7 +677,7 @@ lemma mem_closure_iff_exists_list {R} [semiring R] {s : set R} {x} : x ∈ closu
   ⟨[], list.forall_mem_nil _, rfl⟩
   (λ x y ⟨L, HL1, HL2⟩ ⟨M, HM1, HM2⟩, ⟨L ++ M, list.forall_mem_append.2 ⟨HL1, HM1⟩,
     by rw [list.map_append, list.sum_append, HL2, HM2]⟩),
-λ ⟨L, HL1, HL2⟩, HL2 ▸ list_sum_mem _ (λ r hr, let ⟨t, ht1, ht2⟩ := list.mem_map.1 hr in
+λ ⟨L, HL1, HL2⟩, HL2 ▸ list_sum_mem (λ r hr, let ⟨t, ht1, ht2⟩ := list.mem_map.1 hr in
   ht2 ▸ list_prod_mem _ (λ y hy, subset_closure $ HL1 t ht1 y hy))⟩
 
 variable (R)
@@ -899,7 +891,7 @@ lemma range_snd : (snd R S).srange = ⊤ :=
 lemma prod_bot_sup_bot_prod (s : subsemiring R) (t : subsemiring S) :
   (s.prod ⊥) ⊔ (prod ⊥ t) = s.prod t :=
 le_antisymm (sup_le (prod_mono_right s bot_le) (prod_mono_left t bot_le)) $
-assume p hp, prod.fst_mul_snd p ▸ mul_mem _
+assume p hp, prod.fst_mul_snd p ▸ mul_mem
   ((le_sup_left : s.prod ⊥ ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨hp.1, set_like.mem_coe.2 $ one_mem ⊥⟩)
   ((le_sup_right : prod ⊥ t ≤ s.prod ⊥ ⊔ prod ⊥ t) ⟨set_like.mem_coe.2 $ one_mem ⊥, hp.2⟩)