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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
x y : L
⊢ Commute.{u_4} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw : Eq.{u_4 + 1} (α := Module.End R M)
  (Bracket.bracket (L := Module.End R M)
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
    Module.End R M)
  (0 : Module.End R M)
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
x y : L
rw :
  Eq.{u_4 + 1} (α := Module.End R M)
    (Bracket.bracket (L := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
      Module.End R M)
    (0 : Module.End R M)
⊢ Commute.{u_4} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw₁ : Eq.{u_4 + 1} (α := Module.End R M)
  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) ⁅x, y⁆ : Module.End R M)
  (0 : Module.End R M)
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
x y : L
rw :
  Eq.{u_4 + 1} (α := Module.End R M)
    (Bracket.bracket (L := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
      Module.End R M)
    (0 : Module.End R M)
rw₁ :
  Eq.{u_4 + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) ⁅x, y⁆ : Module.End R M)
    (0 : Module.End R M)
⊢ Commute.{u_4} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw₂ : Eq.{u_4 + 1} (α := Module.End R M)
  (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) 0) 0
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
x y : L
rw :
  Eq.{u_4 + 1} (α := Module.End R M)
    (Bracket.bracket (L := Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y) :
      Module.End R M)
    (0 : Module.End R M)
rw₁ :
  Eq.{u_4 + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) ⁅x, y⁆ : Module.End R M)
    (0 : Module.End R M)
rw₂ :
  Eq.{u_4 + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) 0) 0
⊢ Commute.{u_4} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
have rw₃ : Eq.{u_4 + 1} (α := Module.End R M) 0 0
Tactic: rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
⊢ ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
have h : ∀ (x y : L),
  Commute.{u_4} (S := Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
Tactic: have h : ∀ x y, Commute (toEnd R L M x) (toEnd R L M y) := fun x y ↦ by
      rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
h :
  ∀ (x y : L),
    Commute.{u_4} (S := Module.End R M)
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
x y : L
⊢ χ (x + y) = χ x + χ y
have hχ₁ : ¬Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i : L),
      Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) i) (χ i))
    ⊥
Tactic: simp_rw [Ne, ← LieSubmodule.toSubmodule_inj, genWeightSpace, genWeightSpaceOf,
      LieSubmodule.iInf_toSubmodule, LieSubmodule.bot_toSubmodule] at hχ
Cleared hypotheses: hχ
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
⊢ χ (t • x) = t • χ x
have hχ₁ : ¬Eq.{u_4 + 1} (α := Submodule R M)
    (⨅ (i : L),
      Module.End.maxGenEigenspace
        (((toEnd R L M : LieHom.{u_2, u_3, u_4} R L (Module.End R M)) : (a : L) → Module.End R M) i) (χ i))
    ⊥
Tactic: simp_rw [Ne, ← LieSubmodule.toSubmodule_inj, genWeightSpace, genWeightSpaceOf,
        LieSubmodule.iInf_toSubmodule, LieSubmodule.bot_toSubmodule] at hχ
Cleared hypotheses: hχ
-- 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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t x : L
⊢ χ ⁅t, x⁆ = 0
have rw : χ 0 = 0
Tactic: rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t x : L
rw : χ 0 = 0
⊢ χ ⁅t, x⁆ = 0
have rw₁ : χ 0 + χ 0 = 0 + χ 0
Tactic: rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t x : L
rw : χ 0 = 0
rw₁ : χ 0 + χ 0 = 0 + χ 0
⊢ χ ⁅t, x⁆ = 0
have rw₂ : χ (HAdd.hAdd (α := L) 0 0) = 0 + χ 0
Tactic: rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t x : L
rw : χ 0 = 0
rw₁ : χ 0 + χ 0 = 0 + χ 0
rw₂ : χ (HAdd.hAdd (α := L) 0 0) = 0 + χ 0
⊢ χ ⁅t, x⁆ = 0
have rw₃ : χ 0 = 0 + χ 0
Tactic: rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_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 : IsLieAbelian L
inst_8 : IsDomain R
inst_9 : Module.IsTorsionFree R M
aux : ∀ (χ : L → R), Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥ → ∀ (x y : L), χ (x + y) = χ x + χ y
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t x : L
rw : χ 0 = 0
rw₁ : χ 0 + χ 0 = 0 + χ 0
rw₂ : χ (HAdd.hAdd (α := L) 0 0) = 0 + χ 0
rw₃ : χ 0 = 0 + χ 0
⊢ χ ⁅t, x⁆ = 0
have rw₄ : χ 0 = χ 0
Tactic: rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
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
χ : L → 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) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ
have h : ∀ (x : L),
  ((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 =
    (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
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
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
⊢ 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
have rwa : ∀ (hχ : Nontrivial.{u_4} ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
Tactic: rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
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
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
rwa : ∀ (hχ : Nontrivial.{u_4} ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
have rwa₁ : ∀ (hχ : 0 < Module.rank R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
Tactic: rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
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
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
rwa : ∀ (hχ : Nontrivial.{u_4} ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₁ : ∀ (hχ : 0 < Module.rank R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
have rwa₂ : ∀ (hχ : LT.lt.{u_4 + 1} (α := Cardinal.{u_4}) 0 (↑(finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) : Cardinal.{u_4})),
  0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
Tactic: rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ
Cleared hypotheses: hχ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
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
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
rwa : ∀ (hχ : Nontrivial.{u_4} ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₁ : ∀ (hχ : 0 < Module.rank R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
rwa₂ :
  ∀ (hχ : LT.lt.{u_4 + 1} (α := Cardinal.{u_4}) 0 (↑(finrank.{u_2, u_4} R ↥(genWeightSpace M χ)) : Cardinal.{u_4})),
    0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
⊢ 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
have rwa₃ : ∀ (hχ : 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)), 0 < finrank.{u_2, u_4} R ↥(genWeightSpace M χ)
Tactic: rwa [← LieSubmodule.nontrivial_iff_ne_bot, ← rank_pos_iff_nontrivial (R := R), ← finrank_eq_rank,
    Nat.cast_pos] at hχ
Cleared hypotheses: hχ
-- 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) = χ x + χ y
have rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • (χ x + χ y)
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 χ) ⊥
x y : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • (χ x + χ y)
⊢ χ (x + y) = χ x + χ y
have 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
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 χ) ⊥
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
⊢ χ (x + y) = χ x + χ y
have 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
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 χ) ⊥
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
⊢ χ (x + y) = χ x + χ y
have 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
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 χ) ⊥
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
⊢ χ (x + y) = χ x + χ y
have 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
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]