awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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) ⊥}
⊢ 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)
have h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
Tactic: have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ 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)
have hds : DirectSum.IsInternal (S := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)
Tactic: have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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.{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)
have 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)
        sorry))
  (∑ x_1 ∈ Finite.toFinset (s := {χ : R | Ne (α := LieSubmodule R L M) (genWeightSpaceOf M χ z) ⊥}) sorry,
    (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: simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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) ⊥}
⊢ 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)
have H : ∀ (h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)),
  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) ⊥}) sorry,
                  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: classical
  have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]
  simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
  exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 H₁ H₂ :
  ∀ (h : iSupIndep.{u_1 + 1, u_4} (α := Submodule R M) fun (i : R) ↦ (↑(genWeightSpaceOf M i z) : Submodule R M)),
    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)
⊢ 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)
have H₃ : ∀ (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.{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) ⊥}) sorry,
                  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: classical
  have h := LieSubmodule.iSupIndep_toSubmodule.mpr <| iSupIndep_genWeightSpaceOf R L M z
  have hds := DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top h <| by
    simp [← LieSubmodule.iSup_toSubmodule]
  simp only [LinearMap.coe_sum, Finset.sum_apply, traceForm_apply_apply,
    LinearMap.trace_eq_sum_trace_restrict' hds hfin hxy]
  exact Finset.sum_congr (by simp) (fun χ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ Membership.mem (γ := Submodule R L) (LinearMap.ker (traceForm R L M)) z
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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
⊢ 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)
have 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)
Tactic: rw [traceForm_apply_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ 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)
have that : IsTorsionFree R A
Tactic: have that : Module.IsTorsionFree R A := .trans_faithfulSMul R (FractionRing R) A
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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.{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)
have 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)
Tactic: rw [← map_zero (algebraMap R A)] at this
Cleared hypotheses: this, that
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← LinearMap.trace_baseChange, LinearMap.baseChange_comp, ← toEnd_baseChange,
    ← toEnd_baseChange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
have hz₁ : Membership.mem (γ := LieSubmodule R L L) (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤) z
Tactic: simp only [lowerCentralSeries_succ, lowerCentralSeries_zero] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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)) (Bracket.bracket (L := LieIdeal A (A ⊗[R] L)) ⊤ ⊤)
    (1 ⊗ₜ[R] z)
have rw : Membership.mem (γ := LieSubmodule A (A ⊗[R] L) (A ⊗[R] L))
  (LieSubmodule.baseChange A (Bracket.bracket (L := LieIdeal R L) ⊤ ⊤)) (1 ⊗ₜ[R] z)
Tactic: rw [← LieSubmodule.baseChange_top, ← LieSubmodule.lie_baseChange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ 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)
have hz₁ : 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
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
have hzc₁ : ∀ (x : L), ⁅x, z⁆ = 0
Tactic: simp only [mem_maxTrivSubmodule] at hzc ⊢
Cleared hypotheses: hzc
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (hypothesis)
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)
⊢ 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)
have hzc₁ : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
Tactic: replace hzc : 1 ⊗ₜ[R] z ∈ LieAlgebra.center A (A ⊗[R] L) := by
    simp only [mem_maxTrivSubmodule] at hzc ⊢
    intro y
    exact y.induction_on rfl (fun a u ↦ by simp [hzc u])
      (fun u v hu hv ↦ by simp [A, hu, hv])
Cleared hypotheses: hzc
-- Lean 4 proof step from Mathlib.Algebra.Lie.TraceForm (goal)
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 : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieAlgebra.center A (A ⊗[R] L)) (1 ⊗ₜ[R] z)
⊢ 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)
have h : Eq (α := Submodule A (A ⊗[R] M))
  (⨆ (μ : A), End.maxGenEigenspace ((toEnd A (A ⊗[R] L) (A ⊗[R] M) : (a : A ⊗[R] L) → End A (A ⊗[R] M)) (1 ⊗ₜ[R] x)) μ)
  ⊤
Tactic: apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero