-- Mathlib/Algebra/Lie/Weights/Linear.lean
lemma toEnd_eq (x : L) :
    toEnd R L (shiftedGenWeightSpace R L M χ) x =
    (shift R L M χ).conj (toEnd R L (genWeightSpace M χ) x - χ x • LinearMap.id)

Proof state:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅x, x✝⁆ = ⁅x, ↑x✝⁆ - χ x • ↑x✝

Tactic:
rfl

Result:
no goals

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
inst✝ : LinearWeights R L M
x : L
⊢ (toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x =
    (shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)

Tactic:
ext

Result:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑(((toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x) x✝) =
    ↑(((shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)) x✝)

Proof state:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑(((toEnd R L ↥(shiftedGenWeightSpace R L M χ)) x) x✝) =
    ↑(((shift R L M χ).conj ((toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id)) x✝)

Tactic:
simp only [toEnd_apply_apply, map_sub, LinearEquiv.conj_apply, map_smul, LinearMap.comp_id,
  LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap,
  LinearMap.sub_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  shift_symm_apply, shift_apply, LinearMap.smul_apply, LinearMap.id_coe, id_eq,
  AddSubgroupClass.coe_sub, SetLike.val_smul]

Result:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅x, x✝⁆ = ↑⁅x, x✝⁆ - χ x • ↑x✝

Proof state:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅x, x✝⁆ = ↑⁅x, x✝⁆ - χ x • ↑x✝

Tactic:
rw [LieSubmodule.coe_bracket]

Result:
case h.a
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
inst✝ : LinearWeights R L M
x : L
x✝ : ↥(shiftedGenWeightSpace R L M χ)
⊢ ↑⁅x, x✝⁆ = ⁅x, ↑x✝⁆ - χ x • ↑x✝