awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
hds : DirectSum.IsInternal (S := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
H :
  Eq (α := R)
    (∑ i ∈ hfin.toFinset (s := {i : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M i z) : Submodule R M) ⊥}),
      (trace R ↥(↑(genWeightSpaceOf M i z) : Submodule R M) :
          (a : ↥(↑(genWeightSpaceOf M i z) : Submodule R M) →ₗ[R] ↥(↑(genWeightSpaceOf M i z) : Submodule R M)) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯))
    (∑ x_1 ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯,
      (trace R ↥(genWeightSpaceOf M x_1 z) : (a : ↥(genWeightSpaceOf M x_1 z) →ₗ[R] ↥(genWeightSpaceOf M x_1 z)) → R)
        (((toEnd.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M x_1 z) :
                LieHom.{u_1, u_3, u_4} R L (End R ↥(genWeightSpaceOf M x_1 z))) :
              (a : L) → End R ↥(genWeightSpaceOf M x_1 z))
            x ∘ₗ
          ((toEnd.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M x_1 z) :
                LieHom.{u_1, u_3, u_4} R L (End R ↥(genWeightSpaceOf M x_1 z))) :
              (a : L) → End R ↥(genWeightSpaceOf M x_1 z))
            y))
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
    ((((∑ χ ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯,
                  traceForm.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M χ z) :
                (a : L) → L →ₗ[R] R)
              x :
            L →ₗ[R] R) :
          (a : L) → R)
        y :
      R)

Tactic:
simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]

Premises used: Finset.sum_apply, LinearMap.coe_sum, LieModule.traceForm_apply_apply, LinearMap.trace_eq_sum_trace_restrict'
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
hds : DirectSum.IsInternal (S := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
⊢ hfin.toFinset (s := {i : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M i z) : Submodule R M) ⊥}) =
    Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : IsPrincipalIdealRing R
inst_10 : IsTorsionFree R M
inst_11 : IsNoetherian R M
inst_12 : IsTriangularizable R L M
z x y : L
hxy :
  ∀ (χ : R),
    MapsTo
      (⇑(((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
        (a : M) → M)
      (↑(genWeightSpaceOf M χ z) : Set M) (↑(genWeightSpaceOf M χ z) : Set M)
hfin : Set.Finite.{u_1} (α := R) {χ : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M χ z) : Submodule R M) ⊥}
h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
hds : DirectSum.IsInternal (S := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
⊢ Eq (α := R)
    (∑ i ∈ hfin.toFinset (s := {i : R | Ne (α := Submodule R M) (↑(genWeightSpaceOf M i z) : Submodule R M) ⊥}),
      (trace R ↥(↑(genWeightSpaceOf M i z) : Submodule R M) :
          (a : ↥(↑(genWeightSpaceOf M i z) : Submodule R M) →ₗ[R] ↥(↑(genWeightSpaceOf M i z) : Submodule R M)) → R)
        (LinearMap.restrict
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y)
          ⋯))
    (∑ x_1 ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) ⋯,
      (trace R ↥(genWeightSpaceOf M x_1 z) : (a : ↥(genWeightSpaceOf M x_1 z) →ₗ[R] ↥(genWeightSpaceOf M x_1 z)) → R)
        (((toEnd.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M x_1 z) :
                LieHom.{u_1, u_3, u_4} R L (End R ↥(genWeightSpaceOf M x_1 z))) :
              (a : L) → End R ↥(genWeightSpaceOf M x_1 z))
            x ∘ₗ
          ((toEnd.{u_1, u_3, u_4} R L ↥(genWeightSpaceOf M x_1 z) :
                LieHom.{u_1, u_3, u_4} R L (End R ↥(genWeightSpaceOf M x_1 z))) :
              (a : L) → End R ↥(genWeightSpaceOf M x_1 z))
            y))

Tactic:
exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) x : R)
      ((0 : (a : L) → R) x : R)
⊢ Membership.mem (γ := Submodule R L) (LinearMap.ker (traceForm R L M)) z

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
h :
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) z : L →ₗ[R] R) : (a : L) → R) x : R)
    ((0 : (a : L) → R) x : R)

Tactic:
rw [traceForm_apply_apply, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    (0 : A)
⊢ IsTorsionFree R A

Tactic:
have that : Module.IsTorsionFree R A := .trans_faithfulSMul R (FractionRing R) A
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    (0 : A)
that : IsTorsionFree R A
⊢ Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    ((algebraMap R A : (a : R) → A) 0 : A)

Tactic:
rw [← map_zero (algebraMap R A)] at this

Premises used: Algebra.algebraMap, map_zero
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    (0 : A)
that : IsTorsionFree R A
this₁ :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    ((algebraMap R A : (a : R) → A) 0 : A)
⊢ IsTorsionFree R A

Tactic:
rw [← map_zero (algebraMap R A)] at this

Premises used: Algebra.algebraMap, map_zero
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    ((algebraMap R A : (a : R) → A) 0 : A)
that : IsTorsionFree R A
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x) :
      R)
    (0 : R)

Tactic:
FaithfulSMul.algebraMap_injective R A this

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
this :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    ((algebraMap R A : (a : R) → A) 0 : A)
that : IsTorsionFree R A
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x) :
      R)
    (0 : R)

Tactic:
exact FaithfulSMul.algebraMap_injective R A this

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
h :
  Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    (0 : A)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x) :
      R)
    (0 : R)

Tactic:
suffices algebraMap R A (trace R _ ((φ z).comp (φ x))) = 0 by
    have that : Module.IsTorsionFree R A := .trans_faithfulSMul R (FractionRing R) A
    rw [← map_zero (algebraMap R A)] at this
    exact FaithfulSMul.algebraMap_injective R A this
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
h :
  Eq.{u_1 + 1} (α := A)
    ((trace A (A ⊗[R] M) : (a : A ⊗[R] M →ₗ[A] A ⊗[R] M) → A)
        ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] z) ∘ₗ
          (toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) :
      A)
    (0 : A)
⊢ Eq (α := A)
    ((algebraMap R A : (a : R) → A)
        ((trace R M : (a : M →ₗ[R] M) → R)
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z ∘ₗ
            ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x)) :
      A)
    (0 : A)

Tactic:
rw [← LinearMap.trace_baseChange, LinearMap.baseChange_comp, ← toEnd_baseChange,
    ← toEnd_baseChange]

Premises used: LinearMap.baseChange_comp, LieModule.toEnd_baseChange, LinearMap.trace_baseChange
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ Membership.mem (γ := LieSubmodule R L L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) z

Tactic:
simp only [lowerCentralSeries_succ, lowerCentralSeries_zero] at hz ⊢

Premises used: LieModule.lowerCentralSeries_zero, LieModule.lowerCentralSeries_succ
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : Membership.mem (γ := LieSubmodule R L L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) z
rw :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L))
    (LieSubmodule.baseChange A (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤)) (1 ⊗ₜ[R] z)
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (Bracket.bracket (L := LieIdeal A (A ⊗[R] L)) ⊤ ⊤)
    (1 ⊗ₜ[R] z)

Tactic:
rw [← LieSubmodule.baseChange_top, ← LieSubmodule.lie_baseChange]

Premises used: LieSubmodule.lie_baseChange, LieSubmodule.baseChange_top
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : Membership.mem (γ := LieSubmodule R L L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) z
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L))
    (LieSubmodule.baseChange A (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤)) (1 ⊗ₜ[R] z)

Tactic:
Submodule.tmul_mem_baseChange_of_mem 1 hz

Premises used: Set.Mem, Submodule.tmul_mem_baseChange_of_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz : Membership.mem (γ := LieSubmodule R L L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) z
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L))
    (LieSubmodule.baseChange A (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤)) (1 ⊗ₜ[R] z)

Tactic:
exact Submodule.tmul_mem_baseChange_of_mem 1 hz

Premises used: Submodule.tmul_mem_baseChange_of_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hz : Membership.mem (γ := LieSubmodule R L L) (lowerCentralSeries R L L 1) z
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)

Tactic:
replace hz : 1 ⊗ₜ z ∈ lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1 := by
    simp only [lowerCentralSeries_succ, lowerCentralSeries_zero] at hz ⊢
    rw [← LieSubmodule.baseChange_top, ← LieSubmodule.lie_baseChange]
    exact Submodule.tmul_mem_baseChange_of_mem 1 hz
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z : L
hzc : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) z
x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
⊢ ∀ (x : L), ⁅x, z⁆ = 0

Tactic:
simp only [mem_maxTrivSubmodule] at hzc ⊢

Premises used: LieModule.mem_maxTrivSubmodule
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : ∀ (x : L), ⁅x, z⁆ = 0
y : A ⊗[R] L
a : A
u : L
⊢ Eq (α := A ⊗[R] L) (Bracket.bracket (L := A ⊗[R] L) (a ⊗ₜ[R] u) (1 ⊗ₜ[R] z)) 0

Tactic:
simp [hzc u]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : ∀ (x : L), ⁅x, z⁆ = 0
y u v : A ⊗[R] L
hu : Eq (α := A ⊗[R] L) ⁅u, 1 ⊗ₜ[R] z⁆ 0
hv : Eq (α := A ⊗[R] L) ⁅v, 1 ⊗ₜ[R] z⁆ 0
⊢ Eq (α := A ⊗[R] L) ⁅u + v, 1 ⊗ₜ[R] z⁆ 0

Tactic:
simp [A, hu, hv]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
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
inst_7 : LieRing.IsNilpotent L
inst_8 : IsDomain R
inst_9 : Free R M
inst_10 : Module.Finite R M
z x : L
A : Type u_1 := AlgebraicClosure (FractionRing R)
hz :
  Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L)) (lowerCentralSeries A (A ⊗[R] L) (A ⊗[R] L) 1) (1 ⊗ₜ[R] z)
hzc : ∀ (x : L), ⁅x, z⁆ = 0
y : A ⊗[R] L
⊢ Eq (α := A ⊗[R] L) ⁅y, 1 ⊗ₜ[R] z⁆ 0

Tactic:
exact y.induction_on rfl (fun a u ↦ by simp [hzc u])
      (fun u v hu hv ↦ by simp [A, hu, hv])