-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
σ : Type u_2
R : Type u_3
L : Type u_4
inst : DecidableEq ι
inst_1 : AddCommMonoid ι
inst_2 : CommRing R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ℒ : ι → Submodule R L
inst_5 : GradedLieAlgebra ℒ
φ : ι →+ R
y : ⨁ (i : ι), ↥(ℒ i)
hM :
  ∀ (k : ι) (b : ⨁ (i : ι), ↥(ℒ i))
    (hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)),
    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
            lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
              HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
          (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
        b =
      HSMul.hSMul (α := R) ((φ : (a : ι) → R) k : R) b
j i : ι
a : ↥(ℒ i)
f : ⨁ (i : ι), ↥(ℒ i)
h : (f : (a : ι) → ↥(ℒ a)) i = 0
h_1 : a ≠ 0
ih :
  (↑((((toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                    lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                      HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                        LinearMap.id :
                  (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                ⁅f, y⁆ :
              ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L) =
    (↑(((⁅f,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                            LinearMap.id :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    y⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
              (a : ι) → ↥(ℒ a))
            j) :
        L) -
      (↑(((⁅y,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                            LinearMap.id :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    f⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
              (a : ι) → ↥(ℒ a))
            j) :
        L)
w :
  (↑((((toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                      lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                        HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                          LinearMap.id :
                    (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                  (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i))
                    (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                          (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        a :
                      ⨁ (i : ι), ↥(ℒ i))
                    y) :
                ⨁ (i : ι), ↥(ℒ i)) :
              (a : ι) → ↥(ℒ a))
            j) :
        L) +
      ((↑(((⁅f,
                    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      y⁆ :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L) -
        (↑(((⁅y,
                    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      f⁆ :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L)) =
    (↑(((Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i))
                    (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                          (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        a :
                      ⨁ (i : ι), ↥(ℒ i))
                    ((toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      y) :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L) +
        (↑(((⁅f,
                    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      y⁆ :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L) -
      ((↑(((⁅y,
                    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                          (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        a)⁆ :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L) +
        (↑(((⁅y,
                    (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                          lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                            HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := Module.End R ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                              LinearMap.id :
                        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      f⁆ :
                  ⨁ (i : ι), ↥(ℒ i)) :
                (a : ι) → ↥(ℒ a))
              j) :
          L))
⊢ (↑((((toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                    lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
                  (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                ⁅HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i))
                    (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                          (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        a :
                      ⨁ (i : ι), ↥(ℒ i))
                    f,
                  y⁆ :
              ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L) =
    (↑((HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
              (⁅HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i))
                    (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                          (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        a :
                      ⨁ (i : ι), ↥(ℒ i))
                    f,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    y⁆ :
                ⨁ (i : ι), ↥(ℒ i))
              (⁅y,
                  (toModule R ι (M := fun (i : ι) ↦ ↥(ℒ i)) (⨁ (i : ι), ↥(ℒ i)) fun (i : ι) ↦
                        lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) i ∘ₗ
                          Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
                      (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                    (HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i))
                      (((of.{u_1, u_4} (fun (i : ι) ↦ ↥(ℒ i)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                            (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                          a :
                        ⨁ (i : ι), ↥(ℒ i))
                      f)⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L)

Tactic:
simp only [Module.End.smulLeft_eq, add_lie, map_add, DirectSum.add_apply, Submodule.coe_add,
          ih, lie_add, DirectSum.sub_apply, AddSubgroupClass.coe_sub]

Premises used: Submodule.coe_add, AddSubgroupClass.coe_sub, DirectSum.sub_apply, map_add, Module.End.smulLeft_eq, DirectSum.add_apply, lie_add, add_lie