-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x_1 : ↥(cartanSubalgebra' b)
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx' :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
hx :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
      Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
        x)
      x hx')
⊢ Eq (α := Submodule R (↥b.support ⊕ ι → R))
    (⨆ (φ : R),
      Module.End.maxGenEigenspace (M := ↥b.support ⊕ ι → R)
        (((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R) :
              ↥(cartanSubalgebra' b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
            (a : ↥(cartanSubalgebra' b)) → Module.End R (↥b.support ⊕ ι → R))
          (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
            Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
            (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
              Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
                (lieAlgebra b) x)
              x hx')
            hx))
        φ)
    ⊤
have obtain : ∀ (d : ↥b.support ⊕ ι → R)
  (hx' :
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      (Matrix.diagonal d))
  (hx :
    Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
        Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
          (lieAlgebra b) x)
        (Matrix.diagonal d) hx')),
  Eq (α := Submodule R (↥b.support ⊕ ι → R))
    (⨆ (φ : R),
      Module.End.maxGenEigenspace (M := ↥b.support ⊕ ι → R)
        (((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R) :
              ↥(cartanSubalgebra' b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
            (a : ↥(cartanSubalgebra' b)) → Module.End R (↥b.support ⊕ ι → R))
          (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
            Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
            (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
              Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
                (lieAlgebra b) x)
              (Matrix.diagonal d) hx')
            hx))
        φ)
    ⊤
Tactic: obtain ⟨d, rfl⟩ : ∃ d : b.support ⊕ ι → R, Matrix.diagonal d = x :=
    span_range_h_le_range_diagonal <| by simpa using hx
Cleared hypotheses: x, hx', hx