-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma trace_toEnd_genWeightSpaceChain_eq_zero
    (hp : genWeightSpace M (p • α + χ) = ⊥)
    (hq : genWeightSpace M (q • α + χ) = ⊥)
    {x : H} (hx : x ∈ corootSpace α) :
    LinearMap.trace R _ (toEnd R H (genWeightSpaceChain M α χ p q) x) = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
hx : x ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x) = 0

Tactic:
induction hx using Submodule.span_induction

Result:
case mem
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x x✝ : ↥H
h✝ : x✝ ∈ {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x✝) = 0

case zero
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) 0) = 0

case add
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x x✝ y✝ : ↥H
hx✝ : x✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
hy✝ : y✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
a✝¹ : (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x✝) = 0
a✝ : (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) y✝) = 0
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) (x✝ + y✝)) = 0

case smul
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
a✝¹ : R
x✝ : ↥H
hx✝ : x✝ ∈ Submodule.span R {x | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}
a✝ : (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) x✝) = 0
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) (a✝¹ • x✝)) = 0

Proof state:
case h.a
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ⁅⁅y, z⁆, ↑x✝⁆ = ↑(⁅f, g⁆ x✝)

Tactic:
simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
AddSubgroupClass.coe_sub, f, g]

Result:
no goals

Proof state:
case h.a
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ↑(((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) x✝) = ↑(⁅f, g⁆ x✝)

Tactic:
rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]

Result:
case h.a
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
f : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
g : End R ↥(genWeightSpaceChain M α χ p q) :=
  {
    toFun := fun x =>
      match x with
      | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩,
    map_add' := ⋯, map_smul' := ⋯ }
x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ ⁅⁅y, z⁆, ↑x✝⁆ = ↑(⁅f, g⁆ x✝)

Proof state:
case zero
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsNoetherian R L
hp : genWeightSpace M (p • α + χ) = ⊥
hq : genWeightSpace M (q • α + χ) = ⊥
x : ↥H
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) 0) = 0

Tactic:
simp

Result:
no goals