-- Module: Mathlib.Algebra.Lie.Weights.Chain
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
H : LieSubalgebra R L
α χ : ↥H → R
p q : ℤ
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
hp : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (p • α + χ)) ⊥
hq : Eq (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M (q • α + χ)) ⊥
x : ↥H
hx :
  Membership.mem (γ := Submodule R ↥H)
    (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x
mem :
  ∀ (u : ↥H)
    (hu : Membership.mem (γ := Set ↥H) {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)} u),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
            (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
          (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                  LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
              u :
            End R ↥(genWeightSpaceChain M α χ p q)) :
        R)
      (0 : R)
zero :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
              LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
            (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
          0) :
      R)
    (0 : R)
add :
  ∀ (x y : ↥H),
    Membership.mem (γ := Submodule R ↥H)
        (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x →
      Membership.mem (γ := Submodule R ↥H)
          (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) y →
        Eq.{u_1 + 1} (α := R)
            ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
                  (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
                (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                        LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                      (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                    x :
                  End R ↥(genWeightSpaceChain M α χ p q)) :
              R)
            (0 : R) →
          Eq.{u_1 + 1} (α := R)
              ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
                    (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
                  (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                          LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                        (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                      y :
                    End R ↥(genWeightSpaceChain M α χ p q)) :
                R)
              (0 : R) →
            Eq.{u_1 + 1} (α := R)
              ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
                    (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
                  (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                          LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                        (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                      (x + y) :
                    End R ↥(genWeightSpaceChain M α χ p q)) :
                R)
              (0 : R)
smul :
  ∀ (a : R) (x : ↥H),
    Membership.mem (γ := Submodule R ↥H)
        (Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = (↑x : L)}) x →
      Eq.{u_1 + 1} (α := R)
          ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
                (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
              (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                      LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                    (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                  x :
                End R ↥(genWeightSpaceChain M α χ p q)) :
            R)
          (0 : R) →
        Eq.{u_1 + 1} (α := R)
          ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
                (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
              (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                      LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
                    (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
                  (a • x) :
                End R ↥(genWeightSpaceChain M α χ p q)) :
            R)
          (0 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R ↥(genWeightSpaceChain M α χ p q) :
          (a : ↥(genWeightSpaceChain M α χ p q) →ₗ[R] ↥(genWeightSpaceChain M α χ p q)) → R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpaceChain M α χ p q) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpaceChain M α χ p q))) :
              (a : ↥H) → End R ↥(genWeightSpaceChain M α χ p q))
            x :
          End R ↥(genWeightSpaceChain M α χ p q)) :
      R)
    (0 : R)

Tactic:
induction hx using Submodule.span_induction with
  | mem u hu =>
    obtain ⟨y, hy, z, hz, hyz⟩ := hu
    let f : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(y : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M α χ p q hq hy hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    let g : Module.End R (genWeightSpaceChain M α χ p q) :=
      { toFun := fun ⟨m, hm⟩ ↦ ⟨⁅(z : L), m⁆,
          lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left M α χ p q hp hz hm⟩
        map_add' := fun _ _ ↦ by simp
        map_smul' := fun t m ↦ by simp }
    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]
    simp [hfg]
  | zero => simp
  | add => simp_all
  | smul => simp_all