-- 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 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' := ⋯ }
x✝¹ x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ (fun x =>
        match x with
        | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩)
      (x✝¹ + x✝) =
    (fun x =>
          match x with
          | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩)
        x✝¹ +
      (fun x =>
          match x with
          | ⟨m, hm⟩ => ⟨⁅z, m⁆, ⋯⟩)
        x✝

Tactic:
simp

Result:
no goals

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 u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
t : R
m : ↥(genWeightSpaceChain M α χ p q)
⊢ {
          toFun := fun x =>
            match x with
            | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
          map_add' := ⋯ }.toFun
      (t • m) =
    (RingHom.id R) t •
      {
            toFun := fun x =>
              match x with
              | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩,
            map_add' := ⋯ }.toFun
        m

Tactic:
simp

Result:
no goals

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 u : ↥H
y : L
hy : y ∈ rootSpace H α
z : L
hz : z ∈ rootSpace H (-α)
hyz : ⁅y, z⁆ = ↑u
x✝¹ x✝ : ↥(genWeightSpaceChain M α χ p q)
⊢ (fun x =>
        match x with
        | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩)
      (x✝¹ + x✝) =
    (fun x =>
          match x with
          | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩)
        x✝¹ +
      (fun x =>
          match x with
          | ⟨m, hm⟩ => ⟨⁅y, m⁆, ⋯⟩)
        x✝

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
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' := ⋯ }
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) = 0

Tactic:
have hfg : toEnd R H _ u = ⁅f, g⁆ := by
  ext
  rw [toEnd_apply_apply, LieSubmodule.coe_bracket, LieSubalgebra.coe_bracket_of_module, ← hyz]
  simp only [lie_lie, LieHom.lie_apply, LinearMap.coe_mk, AddHom.coe_mk, Module.End.lie_apply,
  AddSubgroupClass.coe_sub, f, g]

Result:
case intro.intro.intro.intro
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' := ⋯ }
hfg : (toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u = ⁅f, g⁆
⊢ (LinearMap.trace R ↥(genWeightSpaceChain M α χ p q)) ((toEnd R ↥H ↥(genWeightSpaceChain M α χ p q)) u) = 0

Proof state:
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

Tactic:
simp_all

Result:
no goals