-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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')
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))
          φ)
      ⊤
⊢ 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))
        φ)
    ⊤

Tactic:
obtain ⟨d, rfl⟩ : ∃ d : b.support ⊕ ι → R, Matrix.diagonal d = x :=
    span_range_h_le_range_diagonal <| by simpa using hx

Premises used: RootPairing.GeckConstruction.span_range_h_le_range_diagonal, rfl