awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁆ - χ y • m⁆ - χ x • (⁅y, m⁆ - χ y • m) =
    ⁅⁅x, y⁆, m⁆ - χ ⁅x, y⁆ • m + (⁅y, ⁅x, m⁆ - χ x • m⁆ - χ y • (⁅x, m⁆ - χ x • 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⁆ - χ y • m⁆ - χ x • (⁅y, m⁆ - χ y • m) =
    ⁅⁅x, y⁆, m⁆ - χ ⁅x, y⁆ • m + (⁅y, ⁅x, m⁆ - χ x • m⁆ - χ y • (⁅x, m⁆ - χ x • m))
have simp : ⁅x, ⁅y, m⁆⁆ - χ y • ⁅x, m⁆ - (χ x • ⁅y, m⁆ - χ y • χ x • m) =
  ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ + (⁅y, ⁅x, m⁆⁆ - χ x • ⁅y, m⁆ - (χ y • ⁅x, m⁆ - χ y • χ x • m))
Tactic: simp only [lie_sub, lie_smul, lie_lie, LinearWeights.map_lie χ (aux R L M χ), zero_smul,
      sub_zero, smul_sub, smul_comm (χ x)]
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, m⁆ = t • ⁅x, 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have a : (↑⁅t • x, m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
Tactic: apply Subtype.ext
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ (↑⁅t • x, m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
have a : ⁅t • x, (↑m : M)⁆ - χ (t • x) • (↑m : M) = (↑(t • ⁅x, m⁆) : M)
Tactic: rw [coe_lie_shiftedGenWeightSpace_apply]
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅t • x, (↑m : M)⁆ - χ (t • x) • (↑m : M) = (↑(t • ⁅x, m⁆) : M)
have a : t • ⁅x, (↑m : M)⁆ - t • χ x • (↑m : M) = t • (↑⁅x, m⁆ : M)
Tactic: simp only [smul_lie, LinearWeights.map_smul χ (aux R L M χ), smul_assoc t, SetLike.val_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 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ t • ⁅x, (↑m : M)⁆ - t • χ x • (↑m : M) = t • (↑⁅x, m⁆ : M)
have a : t • (⁅x, (↑m : M)⁆ - χ x • (↑m : M)) = t • (↑⁅x, m⁆ : M)
Tactic: rw [← smul_sub]
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, t • m⁆ = t • ⁅x, 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
have a : (↑⁅x, t • m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
Tactic: apply Subtype.ext
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ (↑⁅x, t • m⁆ : M) = (↑(t • ⁅x, m⁆) : M)
have a : ⁅x, (↑(t • m) : M)⁆ - χ x • (↑(t • m) : M) = (↑(t • ⁅x, m⁆) : M)
Tactic: rw [coe_lie_shiftedGenWeightSpace_apply]
-- 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
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ ⁅x, (↑(t • m) : M)⁆ - χ x • (↑(t • m) : M) = (↑(t • ⁅x, m⁆) : M)
have a : t • ⁅x, (↑m : M)⁆ - χ x • t • (↑m : M) = t • (↑⁅x, m⁆ : M)
Tactic: simp only [SetLike.val_smul, lie_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 : LieRing.IsNilpotent L
χ : L → R
inst_8 : LinearWeights R L M
t : R
x : L
m : ↥(shiftedGenWeightSpace R L M χ)
h : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M χ)
⊢ t • ⁅x, (↑m : M)⁆ - χ x • t • (↑m : M) = t • (↑⁅x, m⁆ : M)
have a : t • (⁅x, (↑m : M)⁆ - χ x • (↑m : M)) = t • (↑⁅x, m⁆ : M)
Tactic: rw [smul_comm (χ x), ← smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (hypothesis)
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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
Tactic: replace hχ : Nontrivial (shiftedGenWeightSpace R L M χ) :=
    (LieSubmodule.nontrivial_iff_ne_bot R L M).mpr χ.genWeightSpace_ne_bot
-- 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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have obtain : ∀ (m : M) (property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m)
  (hm₁ :
    Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
      (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property))
  (hm₂ :
    Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
        Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
          (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
        hm₁ ≠
      0),
  ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
Tactic: obtain ⟨⟨⟨m, _⟩, hm₁⟩, hm₂⟩ :=
    @exists_ne _ (nontrivial_max_triv_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)) 0
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (hypothesis)
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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁ :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁ ≠
    0
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have hm₃ : ∀ (x : L),
  (↑⁅x,
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
      M) =
    0
Tactic: simp_rw [mem_maxTrivSubmodule, Subtype.ext_iff,
    ZeroMemClass.coe_zero] at hm₁
-- 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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
⊢ ∃ (m : M), m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have refine : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
Tactic: refine ⟨m, by simpa [LieSubmodule.mk_eq_zero] using hm₂, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (hypothesis)
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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
x : L
⊢ ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have this : (↑⁅x,
        Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
    M) =
  0
Tactic: have := hm₁ 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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
x : L
this :
  (↑⁅x,
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
      M) =
    0
⊢ ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have rwa : ∀
  (this :
    ⁅x,
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                property) :
            M)⁆ -
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R)
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                property) :
            M) =
      0),
  ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
Tactic: rwa [coe_lie_shiftedGenWeightSpace_apply, sub_eq_zero] at this
Cleared hypotheses: this
-- 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 : LieRing.IsNilpotent L
inst_8 : LinearWeights R L M
inst_9 : IsNoetherian R M
χ : Weight R L M
hχ : Nontrivial.{u_4} ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))
m : M
property : Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) m
hm₁_1 :
  Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
    (Subtype.mk (p := fun (x : M) ↦
      Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
hm₂ :
  Subtype.mk (p := fun (x : ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) ↦
      Membership.mem (γ := LieSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)))
        (maxTrivSubmodule R L ↥(shiftedGenWeightSpace R L M (⇑χ : (a : L) → R))) x)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property)
      hm₁_1 ≠
    0
hm₁ :
  ∀ (x : L),
    (↑⁅x,
            Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
        M) =
      0
x : L
this :
  (↑⁅x,
          Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property⁆ :
      M) =
    0
rwa :
  ∀
    (this :
      ⁅x,
            (↑(Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                  property) :
              M)⁆ -
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R)
            (↑(Subtype.mk (p := fun (x : M) ↦
                  Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m
                  property) :
              M) =
        0),
    ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
⊢ ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
have rwa₁ : ∀
  (this :
    ⁅x,
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property) :
          M)⁆ =
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R)
        (↑(Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := LieSubmodule R L M) (shiftedGenWeightSpace R L M (⇑χ : (a : L) → R)) x) m property) :
          M)),
  ⁅x, m⁆ = HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((χ : (a : L) → R) x : R) m
Tactic: rwa [coe_lie_shiftedGenWeightSpace_apply, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
⊢ Nonempty (Weight k L M)
have by_contra! : ∀ (contra : IsEmpty (Weight k L M)), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
have obtain : ∀ (χ : Weight k L M), ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
Tactic: obtain ⟨χ⟩ : Nonempty (Weight k L M) := by
    by_contra! contra
    simpa only [iSup_of_empty, bot_ne_top] using LieModule.iSup_genWeightSpace_eq_top' k L M
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
have obtain : ∀ (m : M) (hm₀ : m ≠ 0) (hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m),
  ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
Tactic: obtain ⟨m, hm₀, hm⟩ := exists_forall_lie_eq_smul k L M χ
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
Goal:
k : Type u_1
L : Type u_3
M : Type u_4
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
inst_3 : LieRing.IsNilpotent L
inst_4 : Field k
inst_5 : LieAlgebra k L
inst_6 : Module k M
inst_7 : Module.Finite k M
inst_8 : LieModule k L M
inst_9 : LinearWeights k L M
inst_10 : IsTriangularizable k L M
inst_11 : Nontrivial M
χ : Weight k L M
m : M
hm₀ : m ≠ 0
hm : ∀ (x : L), ⁅x, m⁆ = HSMul.hSMul.{u_1, u_4, u_4} (α := k) ((χ : (a : L) → k) x : k) m
⊢ ∃ (χ : Module.Dual k L), Nontrivial.{u_4} ↥(weightSpace M (⇑χ : (a : L) → k))
have simp : ∃ (χ : Module.Dual k L) (x : M) (_ : Membership.mem (γ := LieSubmodule k L M) (weightSpace M (⇑χ : (a : L) → k)) x),
  ¬x = 0
Tactic: simp only [LieSubmodule.nontrivial_iff_ne_bot, LieSubmodule.eq_bot_iff, ne_eq, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
have pos : ∀ (hx' : x = 0), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
Tactic: by_cases hx' : x = 0