refactor(Lie/Graded): remove a redundant assumption (leanprover-community#38120)

The equality pattern can be helpful when working with families of types, but provides little value when working with families of submodules. Indeed, the only caller passes `rfl`, and any family implementing this interface can use `let +generalize k := i + j` if they really find it useful.

Also adds an implementation note that remarks the design is divergent from GradedModule and GradedMonoid.

I think we should correct this divergence, but it's not at all urgent.

Author: eric-wieser

Mathlib/Algebra/Lie/Graded.lean

@@ -12,9 +12,7 @@ public import Mathlib.Algebra.Lie.Derivation.Basic
 # Graded Lie algebras
 
 This file defines typeclasses `SetLike.GradedBracket` and `GradedLieAlgebra`, for working with Lie
-algebras that are graded by a collection `ℒ` of submodules. The additivity of degree with respect to
-the bracket product is encoded by an addition condition so we can avoid the usual difficulties of
-adding elements of `A (i + j)` to elements of `A (j + i)`.
+algebras that are graded by a collection `ℒ` of submodules.
 
 ## Main definitions
 
@@ -25,6 +23,12 @@ adding elements of `A (i + j)` to elements of `A (j + i)`.
 * `LieDerivation.ofGrading`: A Lie derivation on a graded Lie algebra, that scalar-multiplies graded
   pieces by an additive map applied to degree.
 
+## Implementation notes
+
+For now we only implement internally-graded Lie algebras; supporting the externally-graded case
+would be achieved by generalizing the `LieRing (⨁ i, ℒ i)` instance to take a family of types,
+and defining a new `GradedMonoid.GBracket` class to provide the data piecewise.
+
 -/
 
 @[expose] public section
@@ -38,7 +42,7 @@ section SetLike
 /-- A class that ensures a bracket product preserves an additive grading. -/
 class SetLike.GradedBracket [SetLike σ L] [Bracket L L] [Add ι] (ℒ : ι → σ) : Prop where
   /-- Bracket is homogeneous -/
-  bracket_mem : ∀ ⦃i j k⦄ {gi gj}, i + j = k → gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ k
+  bracket_mem : ∀ ⦃i j⦄ {gi gj}, gi ∈ ℒ i → gj ∈ ℒ j → ⁅gi, gj⁆ ∈ ℒ (i + j)
 
 variable [DecidableEq ι] [AddCommMonoid ι] [CommRing R] [LieRing L] [LieAlgebra R L]
   (ℒ : ι → Submodule R L)
@@ -125,7 +129,7 @@ def ofGradingSum (φ : ι →+ R) : LieDerivation R (⨁ i, ℒ i) (⨁ i, ℒ i
             add_lie, smul_add, add_sub, ← sub_sub]
           congr 1
           have : (decompose ℒ).symm ⁅of (fun i ↦ ℒ i) i a, of (fun i ↦ ℒ i) k b⁆ ∈ ℒ (i + k) := by
-            simp [SetLike.GradedBracket.bracket_mem rfl (Submodule.coe_mem a) (Submodule.coe_mem b)]
+            simp [SetLike.GradedBracket.bracket_mem (Submodule.coe_mem a) (Submodule.coe_mem b)]
           rw [hM _ _ this, hM k (of (ℒ ·) k b) (by simp), ← lie_skew (of (ℒ ·) k b),
             add_sub_right_comm, add_right_cancel_iff, add_comm i k, map_add, add_smul,
             DirectSum.add_apply, Submodule.coe_add, sub_eq_add_neg, lie_smul, add_left_cancel_iff,