awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
w :
  ∀ (j : ι),
    (↑((((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)
⊢ (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⁆ =
    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))

Tactic:
ext j
-- 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 : ι
⊢ (↑((((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)

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
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)
⊢ Membership.mem (α := L) (ℒ i)
    ((Equiv.symm (decompose ℒ) : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
        (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i)) a :
          ⨁ (i : ι), ↥(ℒ i)) :
      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 ℒ
φ : ι →+ R
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
⊢ (↑(((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))
                0) :
            (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))
                  0) :
              (a : ι) → ↥(ℒ a))
            j) :
        L) -
      (↑((Bracket.bracket (L := ⨁ (i : ι), ↥(ℒ i)) 0
                (HSMul.hSMul (α := R) (β := ⨁ (i : ι), ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
                  (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) :
                        (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                      a :
                    ⨁ (i : ι), ↥(ℒ i))) :
              (a : ι) → ↥(ℒ a))
            j) :
        L)

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 ℒ
φ : ι →+ R
i : ι
a : ↥(ℒ i)
⊢ (ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
      (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i)) a) =
    HSMul.hSMul (α := R) (β := ⨁ (i : ι), ↥(ℒ i)) ((φ : (a : ι) → R) i : R)
      (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i)) a :
        ⨁ (i : ι), ↥(ℒ i))

Tactic:
simp [← lof_eq_of R, ofGradingSum]

Premises used: DirectSum.lof_eq_of, LieDerivation.ofGradingSum
-- 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 x_1 : L
⊢ ((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
      ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
          ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) (x + x_1)) :
        ⨁ (i : ι), ↥(ℒ i)) =
    HAdd.hAdd (α := L) (β := L)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
              ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x) :
            ⨁ (i : ι), ↥(ℒ i)) :
        L)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
              ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x_1) :
            ⨁ (i : ι), ↥(ℒ i)) :
        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 ℒ
φ : ι →+ R
x : R
x_1 : L
⊢ ((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
      ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
          ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) (x • x_1)) :
        ⨁ (i : ι), ↥(ℒ i)) =
    HSMul.hSMul (α := R) (β := L) ((RingHom.id R : (a : R) → R) x : R)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
              ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x_1) :
            ⨁ (i : ι), ↥(ℒ i)) :
        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 ℒ
φ : ι →+ R
x y : L
⊢ ({
          toFun := fun (x : L) ↦
            ((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
              ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                  ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x) :
                ⨁ (i : ι), ↥(ℒ i)),
          map_add' := ⋯, map_smul' := ⋯ } :
        (a : L) → L)
      ⁅x, y⁆ =
    HSub.hSub (α := L) (β := L)
      (⁅x,
          ({
                toFun := fun (x : L) ↦
                  ((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
                    ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x) :
                      ⨁ (i : ι), ↥(ℒ i)),
                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L } :
              (a : L) → L)
            y⁆ :
        L)
      (⁅y,
          ({
                toFun := fun (x : L) ↦
                  ((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
                    ((ofGradingSum ℒ φ : (a : ⨁ (i : ι), ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
                        ((decomposeLinearEquiv ℒ : (a : L) → ⨁ (i : ι), ↥(ℒ i)) x) :
                      ⨁ (i : ι), ↥(ℒ i)),
                map_add' := ⋯, map_smul' := ⋯ : L →ₗ[R] L } :
              (a : L) → L)
            x⁆ :
        L)

Tactic:
simp [decomposeLinearEquiv_apply, decomposeLinearEquiv_symm_apply]

Premises used: DirectSum.decomposeLinearEquiv_apply, 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 ℒ
φ : ι →+ R
i : ι
a : L
ha : a ∈ ℒ i
simp :
  HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := L) ((φ : (a : ι) → R) i : R)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
              (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ i) a ha) :
            ⨁ (i : ι), ↥(ℒ i)) :
        L) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((φ : (a : ι) → R) i : R) a
⊢ (ofGrading ℒ φ : (a : L) → L) a = HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((φ : (a : ι) → R) i : R) a

Tactic:
simp [ofGrading, decomposeLinearEquiv_apply, decompose_of_mem ℒ ha]

Premises used: DirectSum.decompose_of_mem, LieDerivation.ofGrading, 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 ℒ
φ : ι →+ R
i : ι
a : L
ha : a ∈ ℒ i
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := R) (β := L) ((φ : (a : ι) → R) i : R)
      (((decomposeLinearEquiv ℒ).symm : (a : ⨁ (i : ι), ↥(ℒ i)) → L)
          (((of.{u_1, u_4} (fun (x : ι) ↦ ↥(ℒ x)) i : ↥(ℒ i) →+ ⨁ (i : ι), ↥(ℒ i)) : (a : ↥(ℒ i)) → ⨁ (i : ι), ↥(ℒ i))
              (Subtype.mk (p := fun (x : L) ↦ x ∈ ℒ i) a ha) :
            ⨁ (i : ι), ↥(ℒ i)) :
        L) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R) ((φ : (a : ι) → R) i : R) a

Tactic:
simp [decomposeLinearEquiv_symm_apply]

Premises used: DirectSum.decomposeLinearEquiv_symm_apply
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
h : y ∈ I
⊢ ⁅x, y⁆ ∈ I

Tactic:
I.lie_mem h

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
rw : ⁅-y, x⁆ ∈ I
⊢ ⁅x, y⁆ ∈ I

Tactic:
rw [← lie_skew, ← neg_lie]

Premises used: neg_lie, lie_skew
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
h h₁ : x ∈ I
⊢ ⁅-y, x⁆ ∈ I

Tactic:
apply lie_mem_right

Premises used: lie_mem_right
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ x ∈ I

Tactic:
assumption
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
x y : L
_ : x ∈ (↑I : Submodule R L).carrier → y ∈ (↑I : Submodule R L).carrier → ⁅x, y⁆ ∈ (↑I : Submodule R L).carrier
⊢ x ∈ (↑I : Submodule R L).carrier → y ∈ (↑I : Submodule R L).carrier → ⁅x, y⁆ ∈ (↑I : Submodule R L).carrier

Tactic:
_
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
x y : L
h_1 : x ∈ (↑I : Submodule R L).carrier
hy : y ∈ (↑I : Submodule R L).carrier
h : y ∈ I
⊢ ⁅x, y⁆ ∈ (↑I : Submodule R L).carrier

Tactic:
apply lie_mem_right

Premises used: lie_mem_right
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
x y : L
h : x ∈ (↑I : Submodule R L).carrier
hy : y ∈ (↑I : Submodule R L).carrier
⊢ y ∈ I

Tactic:
hy

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
x y : L
h : x ∈ (↑I : Submodule R L).carrier
hy : y ∈ (↑I : Submodule R L).carrier
⊢ y ∈ I

Tactic:
exact hy
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ toLieSubalgebra R L I ↔ x ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ (↑(toLieSubalgebra R L I) : Set L) = (↑I : Set L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
⊢ (toLieSubalgebra R L I).toSubmodule = (↑I : Submodule R L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
M : Type w
inst : AddCommGroup M
R : Type u_1
L : Type u_2
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
I : LieIdeal R L
inst_4 : LieRingModule L M
x : ↥I
m : M
⊢ ⁅x, m⁆ = ⁅(↑x : L), m⁆

Tactic:
LieSubalgebra.coe_bracket_of_module (I : LieSubalgebra R L) x m

Premises used: LieSubalgebra.coe_bracket_of_module, LieIdeal.toLieSubalgebra
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I : LieIdeal R L
⊢ LieModule.{u, v, w} R (↥I) M

Tactic:
LieSubalgebra.lieModule (I : LieSubalgebra R L)

Premises used: Set.Mem, LieSubalgebra.lieModule, LieIdeal.toLieSubalgebra
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
⊢ (∃ (I : LieIdeal R L), LieIdeal.toLieSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
simp only [← toSubmodule_inj, LieIdeal.toLieSubalgebra_toSubmodule,
    Submodule.exists_lieSubmodule_coe_eq_iff L, mem_toSubmodule]

Premises used: Submodule.exists_lieSubmodule_coe_eq_iff, LieSubalgebra.mem_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieSubalgebra.toSubmodule_inj
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
simp : (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
⊢ (∃ (I : LieIdeal R ↥K'), LieIdeal.toLieSubalgebra R (↥K') I = ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]

Premises used: LieSubalgebra.mem_ofLe, LieSubalgebra.coe_bracket, LieSubalgebra.exists_lieIdeal_coe_eq_iff
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
mp : (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) → ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
mpr : (∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K) → ∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K
⊢ (∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

Tactic:
constructor
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Tactic:
h' ⟨x, hx⟩ ⟨y, h hy⟩ hy

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : ↥K'), (↑y : L) ∈ K → ⁅(↑x : L), (↑y : L)⁆ ∈ K
x y : L
hx : x ∈ K'
hy : y ∈ K
⊢ ⁅x, y⁆ ∈ K

Tactic:
exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy

Premises used: Subtype.mk
-- Module: Mathlib.Algebra.Lie.Ideal
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
h' : ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K
x : L
hx : x ∈ K'
y : L
hy : y ∈ K'
hy' : (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') y hy) : L) ∈ K
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') x hx) : L), (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ K') y hy) : L)⁆ ∈ K

Tactic:
h' x y hx hy'

Premises used: Set.Mem