awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
refine :
  LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr I H =
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
refine le_antisymm ?_ (sup_le inf_le_left (iSup₂_le fun _ hα ↦ hα))

Premises used: iSup₂_le, le_antisymm, sup_le
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
rw :
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
    ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K)
| LieSubmodule.restr I H

Tactic:
rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]

Premises used: LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
conv_lhs :
  LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
conv_lhs => rw [lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace]

Premises used: LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpace
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
sup_le_sup_left (iSup₂_le fun α hα ↦ ?_) _

Premises used: sup_le_sup_left, iSup₂_le, Set.Mem, setOf
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
refine :
  ∀ (α : Weight K (↥H) L) (hα : α.IsNonZero),
    LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : Weight K (↥H) L), ⨆ (_ : α.IsNonZero), LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    LieSubmodule.restr I H ⊓ H.toLieSubmodule ⊔
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
refine sup_le_sup_left (iSup₂_le fun α hα ↦ ?_) _

Premises used: sup_le_sup_left, iSup₂_le
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
pos :
  ∀ (h : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
    LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
neg :
  ∀ (h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
    LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
      ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
        ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
          rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
by_cases h : rootSpace H α ≤ I.restr H

Premises used: LieSubmodule.restr, LieAlgebra.rootSpace, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
le_iSup₂_of_le ⟨α, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hα⟩⟩ h inf_le_right

Premises used: Iff.mpr, Finset.mem_univ, Set.Mem, setOf, inf_le_right, Subtype.mk, And.intro, Finset.mem_filter, le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
exact le_iSup₂_of_le ⟨α, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hα⟩⟩ h inf_le_right

Premises used: le_iSup₂_of_le
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
⊢ IsAtom (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L)

Tactic:
have ha := Submodule.isAtom_iff_finrank_eq_one.mpr (finrank_rootSpace_eq_one α hα)
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
ha : IsAtom (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L)
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) = ⊥

Tactic:
have : I.restr H ⊓ rootSpace H (α : H → K) = ⊥ :=
      LieSubmodule.toSubmodule_injective ((ha.not_le_iff_disjoint.mp h).symm.eq_bot)
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
I : LieIdeal K L
α : Weight K (↥H) L
hα : α.IsNonZero
h : ¬rootSpace H (⇑α : (a : ↥H) → K) ≤ LieSubmodule.restr I H
ha : IsAtom (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L)
this : LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) = ⊥
⊢ LieSubmodule.restr I H ⊓ rootSpace H (⇑α : (a : ↥H) → K) ≤
    ⨆ (α : ↥(LieSubalgebra.root : Finset (Weight K (↥H) L))),
      ⨆ (_ : rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K) ≤ LieSubmodule.restr I H),
        rootSpace H (⇑(↑α : Weight K (↥H) L) : (a : ↥H) → K)

Tactic:
simp only [this, bot_le]

Premises used: bot_le
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
χ : Weight R L M
x y : L
⊢ Eq.{u_2 + 1} (α := R) ((χ : (a : L) → R) ⁅x, y⁆ : R) (0 : R)

Tactic:
LinearWeights.map_lie χ χ.genWeightSpace_ne_bot x y

Premises used: LieModule.LinearWeights.map_lie, LieModule.Weight.genWeightSpace_ne_bot, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
χ : Weight R L M
⊢ Eq (α := (a : L) → R) (⇑(toLinear R L M χ) : (a : L) → R) (⇑χ : (a : L) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
χ : Weight R L M
h : χ.IsZero
h₁ : ∀ (x : L), Eq.{u_2 + 1} (α := R) ((toLinear R L M χ : (a : L) → R) x : R) ((0 : (a : L) → R) x : R)
⊢ toLinear R L M χ = 0

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
χ : Weight R L M
h : χ.IsZero
x : L
⊢ Eq.{u_2 + 1} (α := R) ((toLinear R L M χ : (a : L) → R) x : R) ((0 : (a : L) → R) x : R)

Tactic:
simp [h.eq]

Premises used: LieModule.Weight.IsZero.eq
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
χ : Weight R L M
⊢ toLinear R L M χ ≠ 0 ↔ χ.IsNonZero

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
rw₃ rw₄ : Eq.{u_4 + 1} (α := 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)

Tactic:
rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, map_zero]

Premises used: LieHom.map_lie, map_zero, trivial_lie_zero, commute_iff_lie_eq
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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)

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]
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
⊢ ¬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χ

Premises used: LieSubmodule.bot_toSubmodule, LieModule.genWeightSpaceOf, LieSubmodule.iInf_toSubmodule, Ne, LieSubmodule.toSubmodule_inj, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
x y : L
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))
      ⊥
⊢ χ (x + y) = χ x + χ y

Tactic:
Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute
      (toEnd R L M).toLinearMap χ _ hχ h x y

Premises used: Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute, LieModule.toEnd, LieHom.toLinearMap
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
x y : L
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))
      ⊥
⊢ χ (x + y) = χ x + χ y

Tactic:
exact Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute
      (toEnd R L M).toLinearMap χ _ hχ h x y

Premises used: Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute, LieModule.toEnd, LieHom.toLinearMap
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
⊢ ¬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χ

Premises used: LieSubmodule.bot_toSubmodule, LieModule.genWeightSpaceOf, LieSubmodule.iInf_toSubmodule, Ne, LieSubmodule.toSubmodule_inj, LieModule.genWeightSpace
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
t : R
x : L
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))
      ⊥
⊢ χ (t • x) = t • χ x

Tactic:
Module.End.map_smul_of_iInf_genEigenspace_ne_bot
        (toEnd R L M).toLinearMap χ _ hχ t x

Premises used: Module.End.map_smul_of_iInf_genEigenspace_ne_bot, LieModule.toEnd, LieHom.toLinearMap
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
t : R
x : L
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))
      ⊥
⊢ χ (t • x) = t • χ x

Tactic:
exact Module.End.map_smul_of_iInf_genEigenspace_ne_bot
        (toEnd R L M).toLinearMap χ _ hχ t x

Premises used: Module.End.map_smul_of_iInf_genEigenspace_ne_bot, LieModule.toEnd, LieHom.toLinearMap
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
rw₄ rw₅ : χ 0 = χ 0
⊢ χ ⁅t, x⁆ = 0

Tactic:
rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_add]

Premises used: add_left_inj, zero_add, trivial_lie_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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 :
  ∀ (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
⊢ (⇑((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 χ) • χ

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Weights.Linear
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
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:
simp