awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
change :
  (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
⊢ AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) ⁅T, S⁆ =
    ⁅AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) T,
      AddHom.toFun (LinearMap.toAddHom (↑LinearMap.toMatrix' : ((n → R) →ₗ[R] n → R) →ₗ[R] Matrix n n R)) S⁆

Tactic:
change f (T.comp S - S.comp T) = f T * f S - f S * f T

Premises used: HSub.hSub, LinearMap.comp, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
⊢ ∀ (T S : Module.End R (n → R)),
    (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)

Tactic:
have h : ∀ T S : Module.End R _, f (T.comp S) = f T * f S := LinearMap.toMatrix'_comp
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
T S : Module.End R (n → R)
f : ((n → R) →ₗ[R] n → R) ≃ₗ[R] Matrix n n R := LinearMap.toMatrix'
h :
  ∀ (T S : Module.End R (n → R)),
    (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) =
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
rw :
  HSub.hSub (α := Matrix n n R) (β := Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S) : Matrix n n R)
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
rw₁ :
  HSub.hSub (β := Matrix n n R)
      (HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R))
      ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (S ∘ₗ T) : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
rw₂ rw₃ :
  HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
⊢ (f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) (T ∘ₗ S - S ∘ₗ T) =
    HMul.hMul (α := Matrix n n R) (β := Matrix n n R) ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R) -
      HMul.hMul (α := Matrix n n R) (β := Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) S : Matrix n n R)
        ((f : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) T : Matrix n n R)

Tactic:
rw [map_sub, h, h]

Premises used: map_sub
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
f : Module.End R (n → R)
⊢ Eq (α := Matrix n n R) ((lieEquivMatrix' : (a : Module.End R (n → R)) → Matrix n n R) f : Matrix n n R)
    ((LinearMap.toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
A : Matrix n n R
⊢ Eq (α := Module.End R (n → R))
    ((LieEquiv.symm lieEquivMatrix' : (a : Matrix n n R) → Module.End R (n → R)) A : Module.End R (n → R))
    ((Matrix.toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ (P.lieConj h : (a : Matrix n n R) → Matrix n n R) A = P * A * P⁻¹

Tactic:
simp [LinearEquiv.conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
    LinearMap.toMatrix'_toLin']

Premises used: LinearMap.toMatrix'_toLin', Matrix.lieConj, LinearEquiv.conj_apply, LinearMap.toMatrix'_comp
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
P A : Matrix n n R
h : Invertible P
⊢ ((P.lieConj h).symm : (a : Matrix n n R) → Matrix n n R) A = P⁻¹ * A * P

Tactic:
simp [LinearEquiv.symm_conj_apply, Matrix.lieConj, LinearMap.toMatrix'_comp,
    LinearMap.toMatrix'_toLin']

Premises used: LinearMap.toMatrix'_toLin', Matrix.lieConj, LinearEquiv.symm_conj_apply, LinearMap.toMatrix'_comp
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type w₁
inst_3 : DecidableEq m
inst_4 : Fintype m
e : n ≃ m
x x_1 : Matrix n n R
⊢ Eq (α := Matrix m m R) ((reindex e e : (a : Matrix n n R) → Matrix m m R) ⁅x, x_1⁆ : Matrix m m R)
    (Bracket.bracket (L := Matrix m m R) ((reindex e e : (a : Matrix n n R) → Matrix m m R) x : Matrix m m R)
        ((reindex e e : (a : Matrix n n R) → Matrix m m R) x_1) :
      Matrix m m R)

Tactic:
simp only [LieRing.of_associative_ring_bracket, Matrix.reindex_apply,
        Matrix.submatrix_mul_equiv, Matrix.submatrix_sub, Pi.sub_apply]

Premises used: Matrix.submatrix_sub, Matrix.reindex_apply, LieRing.of_associative_ring_bracket, Matrix.submatrix_mul_equiv, Pi.sub_apply
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type w₁
inst_3 : DecidableEq m
inst_4 : Fintype m
e : n ≃ m
M : Matrix n n R
⊢ Eq (α := Matrix m m R) ((reindexLieEquiv e : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)
    ((reindex e e : (a : Matrix n n R) → Matrix m m R) M : Matrix m m R)

Tactic:
rfl

Premises used: Matrix.submatrix, rfl
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type w₁
inst_3 : DecidableEq m
inst_4 : Fintype m
e : n ≃ m
⊢ Eq (α := Matrix m m R ≃ₗ⁅R⁆ Matrix n n R) (LieEquiv.symm (reindexLieEquiv e)) (reindexLieEquiv e.symm)

Tactic:
rfl

Premises used: LieHom.inverse, Matrix.submatrix, LinearMap.inverse, LieEquiv.symm, Matrix.reindexLieEquiv, rfl
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
m : Type w₁
inst_3 : DecidableEq m
inst_4 : Fintype m
e : n ≃ m
x y : Matrix n n R
v : n → R
⊢ x *ᵥ y *ᵥ v = ⁅x, y⁆ *ᵥ v + y *ᵥ x *ᵥ v

Tactic:
simp only [Ring.lie_def, mulVec_mulVec, sub_mulVec, sub_add_cancel]

Premises used: Matrix.sub_mulVec, Ring.lie_def, sub_add_cancel, Matrix.mulVec_mulVec
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
A : Matrix n n R
v : n → R
⊢ ⁅A, v⁆ = A *ᵥ v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
h :
  ∀ (x : Matrix n n R) (i x_1 : n),
    Eq.{u + 1} (α := R)
      (((((toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R)) :
                    (a : Matrix n n R) → Module.End R (n → R))
                  x ∘ₗ
                LinearMap.single R (fun (i : n) ↦ R) i :
              R →ₗ[R] n → R) :
            (a : R) → n → R)
          1 x_1 :
        R)
      ((((LieEquiv.toLieHom (LieEquiv.symm lieEquivMatrix') : (a : Matrix n n R) → Module.End R (n → R)) x ∘ₗ
                LinearMap.single R (fun (i : n) ↦ R) i :
              R →ₗ[R] n → R) :
            (a : R) → n → R)
          1 x_1 :
        R)
⊢ Eq (α := Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))
    (toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))
    (LieEquiv.toLieHom (LieEquiv.symm lieEquivMatrix') : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R))

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
x : Matrix n n R
i x_1 : n
⊢ Eq.{u + 1} (α := R)
    (((((toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R)) :
                  (a : Matrix n n R) → Module.End R (n → R))
                x ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] n → R) :
          (a : R) → n → R)
        1 x_1 :
      R)
    ((((LieEquiv.toLieHom (LieEquiv.symm lieEquivMatrix') : (a : Matrix n n R) → Module.End R (n → R)) x ∘ₗ
              LinearMap.single R (fun (i : n) ↦ R) i :
            R →ₗ[R] n → R) :
          (a : R) → n → R)
        1 x_1 :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Matrix
Goal:
R : Type u
inst : CommRing R
n : Type w
inst_1 : DecidableEq n
inst_2 : Fintype n
⊢ Function.Injective (α := Matrix n n R) (β := Module.End R (n → R))
    (⇑(toEnd R (Matrix n n R) (n → R) : Matrix n n R →ₗ⁅R⁆ Module.End R (n → R)) :
      (a : Matrix n n R) → Module.End R (n → R))

Tactic:
simpa using EmbeddingLike.injective _

Premises used: EmbeddingLike.injective
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N : LieSubmodule R L M
⊢ lcs 0 N = N

Tactic:
rfl

Premises used: Nat.iterate, LieSubmodule.lcs, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs (k + 1) N = Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lcs k N)

Tactic:
Function.iterate_succ_apply' (fun N' => ⁅⊤, N'⁆) k N

Premises used: Function.iterate_succ_apply', Set.Mem, Bracket.bracket, setOf, LieSubmodule.lcs, Top.top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
⊢ lcs 0 (N₁ ⊔ N₂) = lcs 0 N₁ ⊔ lcs 0 N₂

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
k : ℕ
ih : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂
⊢ lcs (k + 1) (N₁ ⊔ N₂) = lcs (k + 1) N₁ ⊔ lcs (k + 1) N₂

Tactic:
simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

Premises used: LieSubmodule.lie_sup, LieSubmodule.lcs_succ
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
N₁ N₂ : LieSubmodule R L M
k : ℕ
zero : lcs 0 (N₁ ⊔ N₂) = lcs 0 N₁ ⊔ lcs 0 N₂
succ : ∀ (k : ℕ) (ih : lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂), lcs (k + 1) (N₁ ⊔ N₂) = lcs (k + 1) N₁ ⊔ lcs (k + 1) N₂
⊢ lcs k (N₁ ⊔ N₂) = lcs k N₁ ⊔ lcs k N₂

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [LieSubmodule.lcs_succ, ih, LieSubmodule.lie_sup]

Premises used: LieSubmodule.lie_sup, LieSubmodule.lcs_succ
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M 0) ⊤

Tactic:
rfl

Premises used: Nat.iterate, LieSubmodule.lcs, LieModule.lowerCentralSeries, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
k : ℕ
⊢ Eq (α := LieSubmodule R L M) (lowerCentralSeries R L M (k + 1))
    (Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k))

Tactic:
(⊤ : LieSubmodule R L M).lcs_succ k

Premises used: Set.Mem, setOf, LieModule.lowerCentralSeries, LieSubmodule.lcs_succ, Top.top
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : x ∈ (↑(Submodule.span R₁ S) : Set M)
⊢ Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x

Tactic:
simp only [SetLike.mem_coe] at hx ⊢

Premises used: SetLike.mem_coe
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0

Tactic:
Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0

Tactic:
exact Submodule.zero_mem _

Premises used: Submodule.zero_mem
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x y z : M
hy₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) y
hz₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) z
hy₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) y
hz₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) z
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (y + z)

Tactic:
Submodule.add_mem _ hy₂ hz₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x y z : M
hy₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) y
hz₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) z
hy₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) y
hz₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) z
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (y + z)

Tactic:
exact Submodule.add_mem _ hy₂ hz₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
y : M
hy : y ∈ S
smul_mem : ∀ (a : L) (b : M) (hb : b ∈ I), Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • ⁅a, b⁆)
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • y)

Tactic:
obtain ⟨a, b, hb, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
smul_mem : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) ⁅c • a, b⁆
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • ⁅a, b⁆)

Tactic:
rw [← smul_lie]

Premises used: smul_lie
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) ⁅c • a, b⁆

Tactic:
Submodule.subset_span ⟨c • a, b, hb, rfl⟩

Premises used: And.intro, Exists.intro, HSMul.hSMul, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
c : R₁
a : L
b : M
hb : b ∈ I
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) ⁅c • a, b⁆

Tactic:
exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R₁ : Type u_1
R₂ : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R₁
inst_1 : CommRing R₂
inst_2 : AddCommGroup M
inst_3 : LieRing L
inst_4 : LieAlgebra R₁ L
inst_5 : LieAlgebra R₂ L
inst_6 : Module R₁ M
inst_7 : Module R₂ M
inst_8 : LieRingModule L M
inst_9 : LieModule R₁ L M
k : ℕ
I : LieSubmodule R₂ L M := lowerCentralSeries R₂ L M k
S : Set M := {x : M | ∃ (a : L), ∃ b ∈ I, ⁅a, b⁆ = x}
x : M
hx : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) x
zero : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) 0
add :
  ∀ (y z : M) (hy₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) y)
    (hz₁ : Membership.mem (γ := Submodule R₁ M) (Submodule.span R₁ S) z)
    (hy₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) y)
    (hz₂ : Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) z),
    Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (y + z)
smul_mem : ∀ (c : R₁) (y : M) (hy : y ∈ S), Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) (c • y)
⊢ Membership.mem (γ := Submodule R₂ M) (Submodule.span R₂ S) x

Tactic:
induction hx using Submodule.closure_induction with
  | zero => exact Submodule.zero_mem _
  | add y z hy₁ hz₁ hy₂ hz₂ => exact Submodule.add_mem _ hy₂ hz₂
  | smul_mem c y hy =>
      obtain ⟨a, b, hb, rfl⟩ := hy
      rw [← smul_lie]
      exact Submodule.subset_span ⟨c • a, b, hb, rfl⟩

Premises used: smul_lie, Submodule.zero_mem, rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ (↑(↑(lowerCentralSeries R L M 0) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M 0) : Submodule ℤ M) : Set M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
ih :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
succ :
  (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) : Submodule R M) : Set M) =
    (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal ℤ L) ⊤ (lowerCentralSeries ℤ L M k)) : Submodule ℤ M) : Set M)
⊢ (↑(↑(lowerCentralSeries R L M (k + 1)) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M (k + 1)) : Submodule ℤ M) : Set M)

Tactic:
rw [lowerCentralSeries_succ, lowerCentralSeries_succ]

Premises used: LieModule.lowerCentralSeries_succ
-- Module: Mathlib.Algebra.Lie.Nilpotent
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
k : ℕ
ih :
  (↑(↑(lowerCentralSeries R L M k) : Submodule R M) : Set M) =
    (↑(↑(lowerCentralSeries ℤ L M k) : Submodule ℤ M) : Set M)
succ :
  (↑(Submodule.span R
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal R L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule R L M) (lowerCentralSeries R L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M) =
    (↑(Submodule.span ℤ
          {x : M |
            ∃ (x_1 : L),
              Membership.mem (γ := LieIdeal ℤ L) ⊤ x_1 ∧
                ∃ (n : M), Membership.mem (γ := LieSubmodule ℤ L M) (lowerCentralSeries ℤ L M k) n ∧ ⁅x_1, n⁆ = x}) :
      Set M)
⊢ (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal R L) ⊤ (lowerCentralSeries R L M k)) : Submodule R M) : Set M) =
    (↑(↑(Bracket.bracket.{v, w} (L := LieIdeal ℤ L) ⊤ (lowerCentralSeries ℤ L M k)) : Submodule ℤ M) : Set M)

Tactic:
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']

Premises used: LieSubmodule.lieIdeal_oper_eq_linear_span'