-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma weightSpace_le_genWeightSpace (χ : L → R) :
    weightSpace M χ ≤ genWeightSpace M χ

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LieSubmodule.toSubmodule_orderEmbedding R L M) (weightSpace M χ) ≤
    (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)

Tactic:
apply (iInf_le _ x).trans

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ ((toEnd R L M) x).eigenspace (χ x) ≤ (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
⊢ weightSpace M χ ≤ genWeightSpace M χ

Tactic:
apply le_iInf

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
⊢ ∀ (i : L), weightSpace M χ ≤ genWeightSpaceOf M (χ i) i

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ ((toEnd R L M) x).eigenspace (χ x) ≤ (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)

Tactic:
exact ((toEnd R L M x).genEigenspace (χ x)).monotone le_top

Result:
no goals

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ weightSpace M χ ≤ genWeightSpaceOf M (χ x) x

Tactic:
rw [← (LieSubmodule.toSubmodule_orderEmbedding R L M).le_iff_le]

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LieSubmodule.toSubmodule_orderEmbedding R L M) (weightSpace M χ) ≤
    (LieSubmodule.toSubmodule_orderEmbedding R L M) (genWeightSpaceOf M (χ x) x)

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
⊢ ∀ (i : L), weightSpace M χ ≤ genWeightSpaceOf M (χ i) i

Tactic:
intro x

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ weightSpace M χ ≤ genWeightSpaceOf M (χ x) x