case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h :
  optParam
    (∀ (m : M) (hm : m ∈ ↑N),
      ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
    (_ :
      ∀ (m : M) (hm : m ∈ ↑N),
        ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
x✝ : { x // x ∈ ↑N }
⊢ ↑(↑(LinearMap.restrict (↑(toEndomorphism R L M) x) h) x✝) = ↑(↑(↑(toEndomorphism R L { x // x ∈ ↑N }) x) x✝)
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h :
  optParam
    (∀ (m : M) (hm : m ∈ ↑N),
      ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
    (_ :
      ∀ (m : M) (hm : m ∈ ↑N),
        ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
⊢ LinearMap.restrict (↑(toEndomorphism R L M) x) h = ↑(toEndomorphism R L { x // x ∈ ↑N }) x
ext
no goals
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
N : LieSubmodule R L M
x : L
h :
  optParam
    (∀ (m : M) (hm : m ∈ ↑N),
      ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
    (_ :
      ∀ (m : M) (hm : m ∈ ↑N),
        ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (Submodule.subtype ↑N)) { val := m, property := hm } ∈ ↑N)
x✝ : { x // x ∈ ↑N }
⊢ ↑(↑(LinearMap.restrict (↑(toEndomorphism R L M) x) h) x✝) = ↑(↑(↑(toEndomorphism R L { x // x ∈ ↑N }) x) x✝)
simp [LinearMap.restrict_apply]