awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • (χ x + χ y)
rw₁ :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₂ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₃ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₄ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x + (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) y
⊢ χ (x + y) = χ x + χ y
have rw₅ : ((LinearMap.trace R ↥(genWeightSpace M χ) :
          LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
        ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
      (a : L) → R)
    (x + y) =
  HAdd.hAdd (α := R) (β := R)
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        x :
      R)
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        y :
      R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_add, ← Pi.smul_apply,
      ← Pi.smul_apply, ← Pi.smul_apply, ← trace_comp_toEnd_genWeightSpace_eq, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
⊢ χ (t • x) = t • χ x
have rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
⊢ χ (t • x) = t • χ x
have rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
⊢ χ (t • x) = t • χ x
have rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
⊢ χ (t • x) = t • χ x
have rw₃ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₃ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x
⊢ χ (t • x) = t • χ x
have rw₄ : ((LinearMap.trace R ↥(genWeightSpace M χ) :
          LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
        ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
      (a : L) → R)
    (t • x) =
  HSMul.hSMul (β := R) t
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        x :
      R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₃ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x
rw₄ :
  ((LinearMap.trace R ↥(genWeightSpace M χ) :
            LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
          ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
        (a : L) → R)
      (t • x) =
    HSMul.hSMul (β := R) t
      (((LinearMap.trace R ↥(genWeightSpace M χ) :
                LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
              ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            (a : L) → R)
          x :
        R)
⊢ χ (t • x) = t • χ x
have rw₅ : HSMul.hSMul (β := R) t
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        x :
      R) =
  HSMul.hSMul (β := R) t
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        x :
      R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
⊢ χ ⁅x, y⁆ = 0
have rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
  HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
⊢ χ ⁅x, y⁆ = 0
have rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
⊢ χ ⁅x, y⁆ = 0
have rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) ⁅x, y⁆ = 0
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) ⁅x, y⁆ = 0
⊢ χ ⁅x, y⁆ = 0
have rw₃ : Eq.{u_2 + 1} (α := R)
  (((LinearMap.trace R ↥(genWeightSpace M χ) :
            LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
          ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
        (a : L) → R)
      ⁅x, y⁆ :
    R)
  (0 : R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) ⁅x, y⁆ = 0
rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        ⁅x, y⁆ :
      R)
    (0 : R)
⊢ χ ⁅x, y⁆ = 0
have rw₄ : Eq.{u_2 + 1} (α := R)
  ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      ((((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            (a : L) → ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ))
          ⁅x, y⁆ :
        ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) :
    R)
  (0 : R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
rw :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ =
    HSMul.hSMul (β := R) (finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) 0
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ ⁅x, y⁆ = 0
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) ⁅x, y⁆ = 0
rw₃ :
  Eq.{u_2 + 1} (α := R)
    (((LinearMap.trace R ↥(genWeightSpace M χ) :
              LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
            ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
          (a : L) → R)
        ⁅x, y⁆ :
      R)
    (0 : R)
rw₄ :
  Eq.{u_2 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
        ((((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
              (a : L) → ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ))
            ⁅x, y⁆ :
          ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) :
      R)
    (0 : R)
⊢ χ ⁅x, y⁆ = 0
have rw₅ : Eq.{u_2 + 1} (α := R)
  ((LinearMap.trace R ↥(genWeightSpace M χ) : (a : ↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) → R)
      (((toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ) : LieHom.{u_2, u_3, u_4} R L (End R ↥(genWeightSpace M χ))) :
            (a : L) → End R ↥(genWeightSpace M χ))
          ⁅x, y⁆ :
        End R ↥(genWeightSpace M χ)) :
    R)
  (0 : R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', nsmul_zero, ← Pi.smul_apply,
      ← trace_comp_toEnd_genWeightSpace_eq, LinearMap.comp_apply, LieHom.coe_toLinearMap,
      LieHom.map_lie, Ring.lie_def, map_sub, LinearMap.trace_mul_comm, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (hypothesis)
Goal:
k : Type u_1
R : Type u_2
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
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x + y, m⁆ - χ (x + y) • m = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)
have a : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
Tactic: nontriviality shiftedGenWeightSpace R L M χ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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
χ : L → R
inst_8 : LinearWeights R L M
x y : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x + y, m⁆ - χ (x + y) • m = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)
have simp : ⁅x, m⁆ + ⁅y, m⁆ - (χ x • m + χ y • m) = ⁅x, m⁆ - χ x • m + (⁅y, m⁆ - χ y • m)
Tactic: simp only [add_lie, LinearWeights.map_add χ (aux R L M χ), add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (hypothesis)
Goal:
k : Type u_1
R : Type u_2
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
χ : L → R
inst_8 : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, m + n⁆ - χ x • (m + n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)
have a : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
Tactic: nontriviality shiftedGenWeightSpace R L M χ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
R : Type u_2
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
χ : L → R
inst_8 : LinearWeights R L M
x : L
m n : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, m + n⁆ - χ x • (m + n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)
have simp : ⁅x, m⁆ + ⁅x, n⁆ - (χ x • m + χ x • n) = ⁅x, m⁆ - χ x • m + (⁅x, n⁆ - χ x • n)
Tactic: simp only [lie_add, smul_add]