-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Chain (goal)
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
inst_7 : H.IsCartanSubalgebra
inst_8 : IsNoetherian R L
inst_9 : IsDomain R
inst_10 : IsPrincipalIdealRing R
inst_11 : CharZero R
inst_12 : IsTorsionFree R M
inst_13 : IsNoetherian R M
hα : α ≠ 0
hχ : Ne (α := LieSubmodule.{u_1, u_2, u_3} R (↥H) M) (genWeightSpace M χ) ⊥
p : ℤ
hp₀ : p < 0
q : ℤ
hq₀ : q > 0
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 : x ∈ corootSpace α
hb : LT.lt (α := ℕ) 0 (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)))
h₁ :
  iSupIndep.{1, u_3} (α := Submodule R M) fun (i : ↥(Finset.Ioo p q)) ↦
    (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) (↑i : ℤ)
h₂ :
  ∀ (i : ℤ),
    MapsTo (⇑((toEnd R (↥H) M : (a : ↥H) → End R M) x : End R M) : (a : M) → M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
      (↑((fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i) : Set M)
h₃ :
  Eq (α := Submodule R M) (↑(genWeightSpaceChain M α χ p q) : Submodule R M)
    (⨆ i ∈ Finset.Ioo p q, (fun (k : ℤ) ↦ ((↑(genWeightSpace M (k • α + χ)) : Submodule R M) : Submodule R M)) i)
⊢ (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
        HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
      x =
    ∑ x_1 ∈ Finset.Ioo p q,
      (LinearMap.trace R ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M) :
          (a :
              ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M) →ₗ[R]
                ↥(↑(genWeightSpace M (x_1 • α + χ)) : Submodule R M)) →
            R)
        (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpace M (x_1 • α + χ)) :
                LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpace M (x_1 • α + χ)))) :
              (a : ↥H) → End R ↥(genWeightSpace M (x_1 • α + χ)))
            x :
          End R ↥(genWeightSpace M (x_1 • α + χ)))
have convert_2 : (HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α +
      HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ)
    x =
  ∑ k ∈ Finset.Ioo p q,
    (LinearMap.trace R ↥(genWeightSpace M (k • α + χ)) :
        (a : ↥(genWeightSpace M (k • α + χ)) →ₗ[R] ↥(genWeightSpace M (k • α + χ))) → R)
      (((toEnd.{u_1, u_2, u_3} R ↥H ↥(genWeightSpace M (k • α + χ)) :
              LieHom.{u_1, u_2, u_3} R (↥H) (End R ↥(genWeightSpace M (k • α + χ)))) :
            (a : ↥H) → End R ↥(genWeightSpace M (k • α + χ)))
          x :
        End R ↥(genWeightSpace M (k • α + χ)))
Tactic: convert_to _ =
    ∑ k ∈ Finset.Ioo p q, (LinearMap.trace R { x // x ∈ (genWeightSpace M (k • α + χ)) })
      ((toEnd R { x // x ∈ H } { x // x ∈ genWeightSpace M (k • α + χ) }) x)