fix(algebra/direct_sum_graded): replace badly-stated and slow simps…

… lemmas with manual ones (#7403)

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simps.20is.20very.20slow/near/236636962). The `simps mul` attribute on `direct_sum.ghas_mul.of_add_subgroups` was taking 44s, only to produce a lemma that wasn't very useful anyway.



Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/direct_sum_graded.lean

@@ -139,8 +139,8 @@ def ghas_one.of_add_submonoids [semiring R] [has_zero ι]
   ghas_one (λ i, carriers i) :=
 { one := ⟨1, one_mem⟩ }
 
+-- `@[simps]` doesn't generate a useful lemma, so we state one manually below.
 /-- Build a `ghas_mul` instance for a collection of `add_submonoids`. -/
-@[simps mul]
 def ghas_mul.of_add_submonoids [semiring R] [has_add ι]
   (carriers : ι → add_submonoid R)
   (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : R) ∈ carriers (i + j)) :
@@ -153,6 +153,12 @@ def ghas_mul.of_add_submonoids [semiring R] [has_add ι]
     map_add' := λ _ _, add_monoid_hom.ext $ λ _, subtype.ext (add_mul _ _ _),
     map_zero' := add_monoid_hom.ext $ λ _, subtype.ext (zero_mul _) }, }
 
+-- `@[simps]` doesn't generate this well
+@[simp] lemma ghas_mul.of_add_submonoids_mul [semiring R] [has_add ι]
+  (carriers : ι → add_submonoid R) (mul_mem) {i j} (a : carriers i) (b : carriers j) :
+  @ghas_mul.mul _ _ _ _ _ (ghas_mul.of_add_submonoids carriers mul_mem) i j a b =
+    ⟨a * b, mul_mem a b⟩ := rfl
+
 /-- Build a `gmonoid` instance for a collection of `add_submonoid`s. -/
 @[simps to_ghas_one to_ghas_mul]
 def gmonoid.of_add_submonoids [semiring R] [add_monoid ι]
@@ -187,14 +193,20 @@ def ghas_one.of_add_subgroups [ring R] [has_zero ι]
   ghas_one (λ i, carriers i) :=
 ghas_one.of_add_submonoids (λ i, (carriers i).to_add_submonoid) one_mem
 
+-- `@[simps]` doesn't generate a useful lemma, so we state one manually below.
 /-- Build a `ghas_mul` instance for a collection of `add_subgroup`s. -/
-@[simps mul]
 def ghas_mul.of_add_subgroups [ring R] [has_add ι]
   (carriers : ι → add_subgroup R)
   (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : R) ∈ carriers (i + j)) :
   ghas_mul (λ i, carriers i) :=
 ghas_mul.of_add_submonoids (λ i, (carriers i).to_add_submonoid) mul_mem
 
+-- `@[simps]` doesn't generate this well
+@[simp] lemma ghas_mul.of_add_subgroups_mul [ring R] [has_add ι]
+  (carriers : ι → add_subgroup R) (mul_mem) {i j} (a : carriers i) (b : carriers j) :
+  @ghas_mul.mul _ _ _ _ _ (ghas_mul.of_add_subgroups carriers mul_mem) i j a b =
+    ⟨a * b, mul_mem a b⟩ := rfl
+
 /-- Build a `gmonoid` instance for a collection of `add_subgroup`s. -/
 @[simps to_ghas_one to_ghas_mul]
 def gmonoid.of_add_subgroups [ring R] [add_monoid ι]
@@ -226,15 +238,22 @@ def ghas_one.of_submodules
   ghas_one (λ i, carriers i) :=
 ghas_one.of_add_submonoids (λ i, (carriers i).to_add_submonoid) one_mem
 
+-- `@[simps]` doesn't generate a useful lemma, so we state one manually below.
 /-- Build a `ghas_mul` instance for a collection of `submodule`s. -/
-@[simps mul]
 def ghas_mul.of_submodules
   [comm_semiring R] [semiring A] [algebra R A] [has_add ι]
   (carriers : ι → submodule R A)
   (mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : A) ∈ carriers (i + j)) :
   ghas_mul (λ i, carriers i) :=
 ghas_mul.of_add_submonoids (λ i, (carriers i).to_add_submonoid) mul_mem
 
+-- `@[simps]` doesn't generate this well
+@[simp] lemma ghas_mul.of_submodules_mul
+  [comm_semiring R] [semiring A] [algebra R A] [has_add ι]
+  (carriers : ι → submodule R A) (mul_mem) {i j} (a : carriers i) (b : carriers j) :
+  @ghas_mul.mul _ _ _ _ _ (ghas_mul.of_submodules carriers mul_mem) i j a b =
+    ⟨a * b, mul_mem a b⟩ := rfl
+
 /-- Build a `gmonoid` instance for a collection of `submodules`s. -/
 @[simps to_ghas_one to_ghas_mul]
 def gmonoid.of_submodules