awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : X
⊢ Eq (α := FreeAlgebra R X)
    (Function.comp (β := FreeAlgebra R X)
      (⇑(AlgHom.comp (B := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
            ((UniversalEnvelopingAlgebra.lift R :
                (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
                  UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
              ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R)))
            ((FreeAlgebra.lift R :
                (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
                  FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
              (Function.comp (β := FreeLieAlgebra R X)
                (⇑(UniversalEnvelopingAlgebra.ι R) :
                  (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                (of R)))) :
        (a : FreeAlgebra R X) → FreeAlgebra R X)
      (FreeAlgebra.ι R) x)
    (Function.comp (β := FreeAlgebra R X) (⇑(AlgHom.id R (FreeAlgebra R X)) : (a : FreeAlgebra R X) → FreeAlgebra R X)
      (FreeAlgebra.ι R) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h :
  ∀ (x : X),
    Eq (α := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
      ((LieHom.comp
              (AlgHom.toLieHom
                (AlgHom.comp (B := FreeAlgebra R X)
                  ((FreeAlgebra.lift R :
                      (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
                        FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                    (Function.comp (β := FreeLieAlgebra R X)
                      (⇑(UniversalEnvelopingAlgebra.ι R) :
                        (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                      (of R)))
                  ((UniversalEnvelopingAlgebra.lift R :
                      (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
                        UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
                    ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X)
                      (FreeAlgebra.ι R)))))
              (UniversalEnvelopingAlgebra.ι R) :
            (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
          (of R x) :
        UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
      ((LieHom.comp (AlgHom.toLieHom (AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))))
              (UniversalEnvelopingAlgebra.ι R) :
            (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
          (of R x) :
        UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
⊢ Eq (α := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    (AlgHom.comp (B := FreeAlgebra R X)
      ((FreeAlgebra.lift R :
          (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
            FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (Function.comp (β := FreeLieAlgebra R X)
          (⇑(UniversalEnvelopingAlgebra.ι R) :
            (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
          (of R)))
      ((UniversalEnvelopingAlgebra.lift R :
          (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
            UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
        ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R))))
    (AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Free
Goal:
R : Type u
X : Type v
inst : CommRing R
L : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : X
⊢ Eq (α := UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    ((LieHom.comp
            (AlgHom.toLieHom
              (AlgHom.comp (B := FreeAlgebra R X)
                ((FreeAlgebra.lift R :
                    (a : X → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X)) →
                      FreeAlgebra R X →ₐ[R] UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                  (Function.comp (β := FreeLieAlgebra R X)
                    (⇑(UniversalEnvelopingAlgebra.ι R) :
                      (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
                    (of R)))
                ((UniversalEnvelopingAlgebra.lift R :
                    (a : FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) →
                      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) →ₐ[R] FreeAlgebra R X)
                  ((lift R : (a : X → FreeAlgebra R X) → FreeLieAlgebra R X →ₗ⁅R⁆ FreeAlgebra R X) (FreeAlgebra.ι R)))))
            (UniversalEnvelopingAlgebra.ι R) :
          (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (of R x) :
      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
    ((LieHom.comp (AlgHom.toLieHom (AlgHom.id R (UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))))
            (UniversalEnvelopingAlgebra.ι R) :
          (a : FreeLieAlgebra R X) → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))
        (of R x) :
      UniversalEnvelopingAlgebra R (FreeLieAlgebra R X))

Tactic:
simp
-- 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 ℒ
x x_1 x_2 : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
      (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) (x + x_1) : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) =
    HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
        ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_1 : L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
        ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- 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 ℒ
x x_1 x_2 : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
      (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) (x_1 + x_2))) =
    HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_1)) :
        ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
        ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- 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 ℒ
x : ⨁ (i : ι), ↥(ℒ i)
⊢ Eq (α := ⨁ (i : ι), ↥(ℒ i))
    ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
        (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
          (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x)) :
      ⨁ (i : ι), ↥(ℒ i))
    (0 : ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- 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 ℒ
x x_1 x_2 : ⨁ (i : ι), ↥(ℒ i)
⊢ (decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
      (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
              (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_1 : L)
                (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
            ⨁ (i : ι), ↥(ℒ i)))) =
    HAdd.hAdd (α := ⨁ (i : ι), ↥(ℒ i)) (β := ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
                ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
                    (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
                      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_1)) :
                  ⨁ (i : ι), ↥(ℒ i)) :
              L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
        ⨁ (i : ι), ↥(ℒ i))
      ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
          (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_1 : L)
            (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
              ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
                  (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
                    (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x_2)) :
                ⨁ (i : ι), ↥(ℒ i)))) :
        ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
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 ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ ⁅x, y⁆ =
    (decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i))
      (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
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 ℒ
x y : L
simp :
  Eq (α := ⨁ (i : ι), ↥(ℒ i)) ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) ⁅x, y⁆ : ⨁ (i : ι), ↥(ℒ i))
    (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i))
        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x : ⨁ (i : ι), ↥(ℒ i))
        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) y) :
      ⨁ (i : ι), ↥(ℒ i))
⊢ Eq (α := ⨁ (i : ι), ↥(ℒ i)) ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) ⁅x, y⁆ : ⨁ (i : ι), ↥(ℒ i))
    (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i)) ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x : ⨁ (i : ι), ↥(ℒ i))
        ((decompose ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) y) :
      ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp only [← decomposeLinearEquiv_apply]

Premises used: DirectSum.decomposeLinearEquiv_apply
-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
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 ℒ
x y : L
⊢ Eq (α := ⨁ (i : ι), ↥(ℒ i)) ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) ⁅x, y⁆ : ⨁ (i : ι), ↥(ℒ i))
    (Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i))
        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x : ⨁ (i : ι), ↥(ℒ i))
        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) y) :
      ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
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 ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
simp :
  Eq.{u_4 + 1} (α := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) ⁅x, y⁆ : L)
    (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y) :
      L)
⊢ Eq.{u_4 + 1} (α := L) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) ⁅x, y⁆ : L)
    (Bracket.bracket (L := L) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y) :
      L)

Tactic:
simp only [← decomposeLinearEquiv_symm_apply]

Premises used: DirectSum.decomposeLinearEquiv_symm_apply
-- Module: Mathlib.Algebra.Lie.Graded
Goal:
ι : Type u_1
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 ℒ
x y : ⨁ (i : ι), ↥(ℒ i)
⊢ Eq.{u_4 + 1} (α := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) ⁅x, y⁆ : L)
    (Bracket.bracket (L := L) (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) x : L)
        (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L) y) :
      L)

Tactic:
simp
-- 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 ℒ
x x_1 : R
x_2 : ⨁ (i : ι), ↥(ℒ i)
⊢ (x + x_1) • x_2 = x • x_2 + x_1 • x_2

Tactic:
simp [add_smul]

Premises used: add_smul
-- 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 ℒ
x : ⨁ (i : ι), ↥(ℒ i)
⊢ HSMul.hSMul (α := R) 0 x = 0

Tactic:
simp
-- 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 ℒ
x : R
x_1 x_2 : ⨁ (i : ι), ↥(ℒ i)
⊢ ⁅x_1, x • x_2⁆ = x • ⁅x_1, x_2⁆

Tactic:
simp
-- 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 ℒ
⊢ ∀ {x y : L},
    (↑(decomposeLinearEquiv ℒ) : L →ₗ[R] ⨁ (i : ι), ↥(ℒ i)).toFun ⁅x, y⁆ =
      ⁅(↑(decomposeLinearEquiv ℒ) : L →ₗ[R] ⨁ (i : ι), ↥(ℒ i)).toFun x,
        (↑(decomposeLinearEquiv ℒ) : L →ₗ[R] ⨁ (i : ι), ↥(ℒ i)).toFun y⁆

Tactic:
simp
-- 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
i : ι
⊢ Membership.mem (α := R) (Set.center R) ((φ : (a : ι) → R) i : R)

Tactic:
simp
-- 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)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)
h :
  ((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
        (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
      (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b) hb) =
    b
⊢ Membership.mem (γ := Submodule R (⨁ (i : ι), ↥(ℒ i)))
    (LinearMap.range (lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k)) b

Tactic:
use ⟨(decompose ℒ).symm b, hb⟩
-- 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)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)
⊢ ((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
        (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
      (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b) hb) =
    b

Tactic:
simp [lof_eq_of, ← decompose_of_mem]

Premises used: DirectSum.decompose_of_mem, DirectSum.lof_eq_of
-- 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)
k : ι
b : ⨁ (i : ι), ↥(ℒ i)
hb : Membership.mem (α := L) (ℒ k) ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L) b : L)
obtain :
  ∀ (w : ↥(ℒ k))
    (hb :
      Membership.mem (α := L) (ℒ k)
        ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
            (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
                  (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
                w :
              ⨁ (i : ι), ↥(ℒ i)) :
          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))
        (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
            (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
          w) =
      HSMul.hSMul (α := R) (β := ⨁ (i : ι), ↥(ℒ i)) ((φ : (a : ι) → R) k : R)
        (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
              (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
            w :
          ⨁ (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) (β := ↥(ℒ i) →ₗ[R] ↥(ℒ i)) ((φ : (a : ι) → R) i : R) LinearMap.id :
        (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      b =
    HSMul.hSMul (α := R) ((φ : (a : ι) → R) k : R) b

Tactic:
obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]

Premises used: Membership.mem, LinearMap.range, Subtype, DirectSum.lof, rfl
-- 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)
k : ι
w : ↥(ℒ k)
hb :
  Membership.mem (α := L) (ℒ k)
    ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
        (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
              (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
            w :
          ⨁ (i : ι), ↥(ℒ i)) :
      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))
      (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
          (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
        w) =
    HSMul.hSMul (α := R) (β := ⨁ (i : ι), ↥(ℒ i)) ((φ : (a : ι) → R) k : R)
      (((lof.{u_3, u_1, u_4} R ι (fun (x : ι) ↦ ↥(ℒ x)) k : ↥(ℒ k) →ₗ[R] ⨁ (i : ι), ↥(ℒ i)) :
            (a : ↥(ℒ k)) → ⨁ (i : ι), ↥(ℒ i))
          w :
        ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp
-- 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)
⊢ ∀ (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

Tactic:
have hM (k : ι) (b : ⨁ i, ℒ i) (hb : (decompose ℒ).symm b ∈ ℒ k) :
          (toModule R ι (⨁ (i : ι), ℒ i) fun i ↦ lof R ι (ℒ ·) i ∘ₗ (φ i • .id)) b = (φ k) • b := by
        obtain ⟨_, rfl⟩ : b ∈ LinearMap.range (lof R ι (ℒ ·) k) := by
          use ⟨(decompose ℒ).symm b, hb⟩
          simp [lof_eq_of, ← decompose_of_mem]
        simp