-- 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 : Fintype ι
inst_10 : DecidableEq ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b)) ∘ₗ
    Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))
this : x ∈ map g (span R (range h'))
rwa :
  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 property)
      hx ∈
    (↑(span R (range h')) : Set ↥(cartanSubalgebra' b))
rwa₁ :
  Membership.mem (α := ↥(lieAlgebra b)) (γ := Set ↥(lieAlgebra b))
    ((⇑(Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))) :
        (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b)) ''
      (↑(span R (range h')) : Set ↥(cartanSubalgebra' b)))
    ((Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b)) :
          (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b))
        (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 property)
          hx) :
      ↥(lieAlgebra b))
rwa₂ :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (image (α := ↥(LieSubalgebra.toSubmodule (lieAlgebra b)))
      (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b))) :
        (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((⇑(Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))) :
          (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b)) ''
        (↑(span R (range h')) : Set ↥(cartanSubalgebra' b))))
    ((Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b)) :
          (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b)) :
            (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b))
          (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 property)
            hx)) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
rwa₃ rwa₄ rwa₅ rwa₆ :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (comp (β := ↥(LieSubalgebra.toSubmodule (lieAlgebra b)))
        (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b))) :
          (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))) :
          (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b)) ''
      (↑(span R (range h')) : Set ↥(cartanSubalgebra' b)))
    ((Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b)) :
          (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b)) :
            (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b))
          (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 property)
            hx)) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (γ := Submodule R ↥(cartanSubalgebra' b)) (span R (range h'))
    (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 property)
      hx)

Tactic:
rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image,
        ← (injective_subtype _).mem_set_image, ← image_comp]

Premises used: Submodule.injective_subtype, SetLike.mem_coe, Set.image_comp, Function.Injective.mem_set_image