-- 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
x 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 : ι
w :
  (↑((((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))
                (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i)) 0 y) :
              ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L) =
    (↑((HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
              (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i)) 0
                  ((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))
                    0⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L)
w₁ :
  ∀ (i : ι) (a : ↥(ℒ i)) (f : ⨁ (i : ι), ↥(ℒ i)),
    (f : (a : ι) → ↥(ℒ a)) i = 0 →
      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 ∘ₗ
                                Module.End.smulLeft ((φ : (a : ι) → R) i) ⋯ :
                            (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                          ⁅f, y⁆ :
                        ⨁ (i : ι), ↥(ℒ i)) :
                      (a : ι) → ↥(ℒ a))
                    j) :
                L) =
              (↑((HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (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))
                              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)
⊢ (↑((((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))
                ⁅x, y⁆ :
              ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L) =
    (↑((HSub.hSub (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
              (⁅x,
                  (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))
                    x⁆ :
                ⨁ (i : ι), ↥(ℒ i)) :
            (a : ι) → ↥(ℒ a))
          j) :
      L)

Tactic:
induction x using DirectSum.induction_on' with
      | h0 => simp
      | hadd i a f _ _ ih =>
        simp only [Module.End.smulLeft_eq, DirectSum.sub_apply, AddSubgroupClass.coe_sub] at ih
        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]
        rw [add_sub_add_comm, add_right_cancel_iff, hM i (of (ℒ ·) i a) (by simp)]
        clear ih
        induction y using DirectSum.induction_on' with
        | h0 => simp
        | hadd k b f _ _ ih =>
          simp only [lie_add, map_add, DirectSum.add_apply, Submodule.coe_add, ih, lie_smul,
            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 (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,
            smul_neg, ← sub_eq_zero, sub_neg_eq_add, ← Submodule.coe_add, Submodule.coe_eq_zero,
            ← DirectSum.add_apply, add_neg_cancel, DirectSum.zero_apply]

Premises used: Submodule.coe_add, AddSubgroupClass.coe_sub, add_neg_cancel, DirectSum.sub_apply, sub_eq_zero, lie_smul, add_sub, sub_eq_add_neg, map_add, smul_neg, add_sub_right_comm, add_left_cancel_iff, sub_sub, add_smul, add_right_cancel_iff, Submodule.coe_eq_zero, add_sub_add_comm, Module.End.smulLeft_eq, DirectSum.add_apply, smul_add, sub_neg_eq_add, lie_add, DirectSum.zero_apply, add_lie