awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
simp :
  {
      toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
          ⁅(↑(t • x) : L), (↑m : M)⁆ ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (β := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) t
      {
        toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : M)⁆ ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }
⊢ {
      toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
          ⁅(↑(t • x) : L), (↑m : M)⁆ ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) ((RingHom.id R : (a : R) → R) t : R)
      {
        toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : M)⁆ ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }

Tactic:
simp only [RingHom.id_apply]

Premises used: RingHom.id_apply
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
h :
  ∀ (m : ↥(genWeightSpace M χ₂)),
    Eq.{u_3 + 1} (α := M)
      (↑(({
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑(t • x) : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
      (↑((HSMul.hSMul (β := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) t
                {
                  toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                    Subtype.mk (p := fun (x : M) ↦
                      Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                      ⁅(↑x : L), (↑m : M)⁆ ⋯,
                  map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) } :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
⊢ {
      toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
          ⁅(↑(t • x) : L), (↑m : M)⁆ ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (β := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) t
      {
        toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x) ⁅(↑x : L), (↑m : M)⁆ ⋯,
        map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) }

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
t : R
x : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ Eq.{u_3 + 1} (α := M)
    (↑(({
              toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                  ⁅(↑(t • x) : L), (↑m : M)⁆ ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
    (↑((HSMul.hSMul (β := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) t
              {
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑x : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ : ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃) } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)

Tactic:
simp only [SetLike.val_smul, smul_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.smul_apply,
      SetLike.mk_smul_mk]

Premises used: LinearMap.coe_mk, LinearMap.smul_apply, smul_lie, SetLike.val_smul, AddHom.coe_mk, SetLike.mk_smul_mk
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
h :
  ∀ (m : ↥(genWeightSpace M χ₂)),
    Eq.{u_3 + 1} (α := M)
      (↑(((AddHom.toFun
                  (LinearMap.toAddHom
                      (rootSpaceWeightSpaceProductAux R L H M hχ :
                        LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                          (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
                    AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
                  ⁅x, y⁆ :
                ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
      (↑(((⁅x,
                  AddHom.toFun
                    (LinearMap.toAddHom
                        (rootSpaceWeightSpaceProductAux R L H M hχ :
                          LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                            (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
                      AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
                    y⁆ :
                ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) :
              (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
            m) :
        M)
⊢ Eq (α := ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))
    (AddHom.toFun
        (LinearMap.toAddHom
            (rootSpaceWeightSpaceProductAux R L H M hχ :
              LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
          AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
        ⁅x, y⁆ :
      ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))
    (⁅x,
        AddHom.toFun
          (LinearMap.toAddHom
              (rootSpaceWeightSpaceProductAux R L H M hχ :
                LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                  (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
            AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
          y⁆ :
      ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
h :
  Eq.{u_3 + 1} (α := M)
    (↑(({
              toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                  ⁅(↑⁅x, y⁆ : L), (↑m : M)⁆ ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
    (↑((⁅x,
              {
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑y : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ }⁆ :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
⊢ Eq.{u_3 + 1} (α := M)
    (↑(((AddHom.toFun
                (LinearMap.toAddHom
                    (rootSpaceWeightSpaceProductAux R L H M hχ :
                      LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                        (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
                  AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
                ⁅x, y⁆ :
              ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
    (↑(((⁅x,
                AddHom.toFun
                  (LinearMap.toAddHom
                      (rootSpaceWeightSpaceProductAux R L H M hχ :
                        LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥(rootSpace H χ₁))
                          (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃))) :
                    AddHom.{u_2, u_3} (↥(rootSpace H χ₁)) (↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)))
                  y⁆ :
              ↥(genWeightSpace M χ₂) →ₗ[R] ↥(genWeightSpace M χ₃)) :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)

Tactic:
simp only [rootSpaceWeightSpaceProductAux]

Premises used: LieAlgebra.rootSpaceWeightSpaceProductAux
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
h : ⁅⁅(↑x : L), (↑y : L)⁆, (↑m : M)⁆ = ⁅(↑x : L), ⁅(↑y : L), (↑m : M)⁆⁆ - ⁅(↑y : L), ⁅(↑x : L), (↑m : M)⁆⁆
⊢ Eq.{u_3 + 1} (α := M)
    (↑(({
              toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                  ⁅(↑⁅x, y⁆ : L), (↑m : M)⁆ ⋯,
              map_add' := ⋯, map_smul' := ⋯ } :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)
    (↑((⁅x,
              {
                toFun := fun (m : ↥(genWeightSpace M χ₂)) ↦
                  Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ₃) x)
                    ⁅(↑y : L), (↑m : M)⁆ ⋯,
                map_add' := ⋯, map_smul' := ⋯ }⁆ :
            (a : ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          m) :
      M)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥H
y : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ ⁅⁅(↑x : L), (↑y : L)⁆, (↑m : M)⁆ = ⁅(↑x : L), ⁅(↑y : L), (↑m : M)⁆⁆ - ⁅(↑y : L), ⁅(↑x : L), (↑m : M)⁆⁆

Tactic:
simp only [lie_lie]

Premises used: lie_lie
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
m : ↥(genWeightSpace M χ₂)
⊢ (↑(((rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ :
              TensorProduct.{u_1, u_2, u_3} R ↥(rootSpace H χ₁) ↥(genWeightSpace M χ₂) →ₗ⁅R,↥H⁆
                ↥(genWeightSpace M χ₃)) :
            (a : ↥(rootSpace H χ₁) ⊗[R] ↥(genWeightSpace M χ₂)) → ↥(genWeightSpace M χ₃))
          (x ⊗ₜ[R] m)) :
      M) =
    ⁅(↑x : L), (↑m : M)⁆

Tactic:
simp only [rootSpaceWeightSpaceProduct, rootSpaceWeightSpaceProductAux, coe_liftLie_eq_lift_coe,
    lift_apply, LinearMap.coe_mk, AddHom.coe_mk]

Premises used: LieAlgebra.rootSpaceWeightSpaceProduct, LinearMap.coe_mk, LieAlgebra.rootSpaceWeightSpaceProductAux, TensorProduct.LieModule.coe_liftLie_eq_lift_coe, TensorProduct.LieModule.lift_apply, AddHom.coe_mk
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ (↑(genWeightSpace M χ) : Set M)
x' : ↥(rootSpace H α) := Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) x hx
m' : ↥(genWeightSpace M χ) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) x) m
    hm
⊢ Membership.mem (α := M) (↑(genWeightSpace M (α + χ)) : Set M)
    (((((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)
        m :
      M)

Tactic:
(rootSpaceWeightSpaceProduct R L H M α χ (α + χ) rfl (x' ⊗ₜ m')).property

Premises used: LieAlgebra.rootSpaceWeightSpaceProduct, Set.Mem, HAdd.hAdd, TensorProduct.tmul, DFunLike.coe, rfl, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
α χ : ↥H → R
x : L
hx : x ∈ rootSpace H α
m : M
hm : m ∈ (↑(genWeightSpace M χ) : Set M)
x' : ↥(rootSpace H α) := Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H α) x hx
m' : ↥(genWeightSpace M χ) :=
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) x) m
    hm
⊢ Membership.mem (α := M) (↑(genWeightSpace M (α + χ)) : Set M)
    (((((toEnd R L M : LieHom.{u_1, u_2, u_3} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)
        m :
      M)

Tactic:
exact (rootSpaceWeightSpaceProduct R L H M α χ (α + χ) rfl (x' ⊗ₜ m')).property

Premises used: LieAlgebra.rootSpaceWeightSpaceProduct, HAdd.hAdd, TensorProduct.tmul, DFunLike.coe, rfl, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
⊢ Eq (α :=
    (χ₁ χ₂ χ₃ : ↥H → R) → (hχ : χ₁ + χ₂ = χ₃) → ↥(rootSpace H χ₁) ⊗[R] ↥(rootSpace H χ₂) →ₗ⁅R,↥H⁆ ↥(rootSpace H χ₃))
    (rootSpaceProduct R L H) (rootSpaceWeightSpaceProduct R L H L)

Tactic:
rfl

Premises used: LieAlgebra.rootSpaceProduct, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
χ₁ χ₂ χ₃ : ↥H → R
hχ : χ₁ + χ₂ = χ₃
x : ↥(rootSpace H χ₁)
y : ↥(rootSpace H χ₂)
⊢ (↑((rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ : (a : ↥(rootSpace H χ₁) ⊗[R] ↥(rootSpace H χ₂)) → ↥(rootSpace H χ₃))
          (x ⊗ₜ[R] y)) :
      L) =
    ⁅(↑x : L), (↑y : L)⁆

Tactic:
simp only [rootSpaceProduct_def, coe_rootSpaceWeightSpaceProduct_tmul]

Premises used: LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul, LieAlgebra.rootSpaceProduct_def
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0) : Submodule R L).carrier
hy : y ∈ (↑(rootSpace H 0) : Submodule R L).carrier
xy : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0) :=
  Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) x hx ⊗ₜ[R] Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy
this :
  (↑((rootSpaceProduct R L H 0 0 0 ⋯ : (a : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0)) → ↥(rootSpace H 0)) xy) : L) ∈
    rootSpace H 0
rwa :
  ∀
    (this :
      ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) x hx) : L),
          (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy) : L)⁆ ∈
        rootSpace H 0),
    ⁅x, y⁆ ∈ (↑(rootSpace H 0) : Submodule R L).carrier
rwa₁ :
  ∀ (this : ⁅x, (↑(Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy) : L)⁆ ∈ rootSpace H 0),
    ⁅x, y⁆ ∈ (↑(rootSpace H 0) : Submodule R L).carrier
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : ⁅x, y⁆ ∈ rootSpace H 0), ⁅x, y⁆ ∈ (↑(rootSpace H 0) : Submodule R L).carrier
⊢ ⁅x, y⁆ ∈ (↑(rootSpace H 0) : Submodule R L).carrier

Tactic:
rwa [rootSpaceProduct_tmul, Subtype.coe_mk, Subtype.coe_mk] at this

Premises used: Subtype.coe_mk, LieAlgebra.rootSpaceProduct_tmul
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0) : Submodule R L).carrier
hy : y ∈ (↑(rootSpace H 0) : Submodule R L).carrier
xy : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0) :=
  Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) x hx ⊗ₜ[R] Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy
suffices :
  (↑((rootSpaceProduct R L H 0 0 0 ⋯ : (a : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0)) → ↥(rootSpace H 0)) xy) : L) ∈
    rootSpace H 0
⊢ ⁅x, y⁆ ∈ (↑(rootSpace H 0) : Submodule R L).carrier

Tactic:
suffices (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy : L) ∈ rootSpace H 0 by
        rwa [rootSpaceProduct_tmul, Subtype.coe_mk, Subtype.coe_mk] at this
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0) : Submodule R L).carrier
hy : y ∈ (↑(rootSpace H 0) : Submodule R L).carrier
xy : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0) :=
  Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) x hx ⊗ₜ[R] Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy
⊢ (↑((rootSpaceProduct R L H 0 0 0 ⋯ : (a : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0)) → ↥(rootSpace H 0)) xy) : L) ∈
    rootSpace H 0

Tactic:
(rootSpaceProduct R L H 0 0 0 (add_zero 0) xy).property

Premises used: LieAlgebra.rootSpaceProduct, add_zero, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
M : Type u_3
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : LieRingModule L M
inst_7 : LieModule R L M
x y : L
hx : x ∈ (↑(rootSpace H 0) : Submodule R L).carrier
hy : y ∈ (↑(rootSpace H 0) : Submodule R L).carrier
xy : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0) :=
  Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) x hx ⊗ₜ[R] Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H 0) y hy
⊢ (↑((rootSpaceProduct R L H 0 0 0 ⋯ : (a : ↥(rootSpace H 0) ⊗[R] ↥(rootSpace H 0)) → ↥(rootSpace H 0)) xy) : L) ∈
    rootSpace H 0

Tactic:
exact (rootSpaceProduct R L H 0 0 0 (add_zero 0) xy).property

Premises used: LieAlgebra.rootSpaceProduct, add_zero, OfNat.ofNat, DFunLike.coe, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
⊢ (zeroRootSubalgebra R L H).toSubmodule = (↑(rootSpace H 0) : Submodule R L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
x : L
⊢ x ∈ rootSpace H 0 ↔
    ∀ (y : ↥H),
      ∃ (k : ℕ),
        Eq (α := L)
          ((HPow.hPow (α := Module.End R L) ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) y : Module.End R L) k :
                (a : L) → L)
              x :
            L)
          (0 : L)

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero]

Premises used: sub_zero, LieModule.mem_genWeightSpace, Pi.zero_apply, zero_smul
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ H.toLieSubmodule
⊢ x ∈ H

Tactic:
simp only [LieSubalgebra.mem_toLieSubmodule] at hx

Premises used: LieSubalgebra.mem_toLieSubmodule
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ H
simp :
  ∀ (x_1 : ↥H),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) x_1 : Module.End R L) k :
              (a : L) → L)
            x :
          L)
        (0 : L)
⊢ x ∈ rootSpace H 0

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, sub_zero, zero_smul]

Premises used: sub_zero, LieModule.mem_genWeightSpace, Pi.zero_apply, zero_smul
-- Module: Mathlib.Algebra.Lie.Weights.Cartan
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : LieRing.IsNilpotent.{u_2} ↥H
x : L
hx : x ∈ H
y : ↥H
obtain :
  ∀ (k : ℕ) (hk : Eq.{u_2 + 1} (α := LieSubmodule R ↥H ↥H) (lowerCentralSeries R (↥H) (↥H) k) ⊥),
    ∃ (k : ℕ),
      Eq (α := L)
        ((HPow.hPow (α := Module.End R L) ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) y : Module.End R L) k :
              (a : L) → L)
            x :
          L)
        (0 : L)
⊢ ∃ (k : ℕ),
    Eq (α := L)
      ((HPow.hPow (α := Module.End R L) ((toEnd R (↥H) L : (a : ↥H) → Module.End R L) y : Module.End R L) k :
            (a : L) → L)
          x :
        L)
      (0 : L)

Tactic:
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R H H

Premises used: Membership.mem, LieModule.IsNilpotent.nilpotent, Subtype