feat(group_theory): use generic subobject_class lemmas (#11758)

This subobject class refactor PR follows up from #11750 by moving the `{zero,one,add,mul,...}_mem_class` lemmas to the root namespace and marking the previous `sub{monoid,group,module,algebra,...}.{zero,one,add,mul,...}_mem` lemmas as `protected`. This is the second part of #11545 to be split off.

I made the subobject parameter to the `_mem` lemmas implicit if it appears in the hypotheses, e.g.
```lean
lemma mul_mem {S M : Type*} [monoid M] [set_like S M] [submonoid_class S M]
  {s : S} {x y : M} (hx : x ∈ s) (hy : y ∈ s) : x * y ∈ s
```
instead of having `(s : S)` explicit. The generic `_mem` lemmas are not namespaced, so there is no dot notation that requires `s` to be explicit. Also there were already a couple of instances for the same operator where `s` was implicit and others where `s` was explicit, so some change was needed.

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

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

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,40 +255,29 @@ 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
 @[simp, norm_cast] lemma coe_algebra_map [comm_semiring R'] [has_scalar R' R] [algebra R' A]
   [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} :

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,

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

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
 

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

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

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