-- 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)
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 =
    ∑ x_1 ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (x_1 • α + χ)) • (x_1 • α + χ) x
convert_2₁ :
  HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) α x +
      HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) χ x =
    ∑ x_1 ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (x_1 • α + χ)) • ((x_1 • α) x + χ x)
convert_2₂ :
  HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) (α x) +
      HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) (χ x) =
    ∑ x_1 ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (x_1 • α + χ)) • (x_1 • α x + χ x)
⊢ (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 • α + χ)))
have convert_2₃ : HSMul.hSMul (α := ℤ) (∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ)) • i) (α x) +
    HSMul.hSMul (α := ℤ) (↑(∑ i ∈ Finset.Ioo p q, finrank.{u_1, u_3} R ↥(genWeightSpace M (i • α + χ))) : ℤ) (χ x) =
  ∑ x_1 ∈ Finset.Ioo p q,
    (finrank.{u_1, u_3} R ↥(genWeightSpace M (x_1 • α + χ)) • x_1 • α x +
      finrank.{u_1, u_3} R ↥(genWeightSpace M (x_1 • α + χ)) • χ x)
Tactic: simp_rw [trace_toEnd_genWeightSpace, Pi.add_apply, Pi.smul_apply, smul_add,
    ← smul_assoc, Finset.sum_add_distrib, ← Finset.sum_smul, natCast_zsmul]