case h
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
K : LieSubalgebra R L
x y : { x // x ∈ K }
⊢ ↑(LinearMap.comp (↑(ad R L) ↑x) ↑(incl K)) y = ↑(LinearMap.comp (↑(incl K)) (↑(ad R { x // x ∈ K }) x)) y
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
K : LieSubalgebra R L
x : { x // x ∈ K }
⊢ LinearMap.comp (↑(ad R L) ↑x) ↑(incl K) = LinearMap.comp (↑(incl K)) (↑(ad R { x // x ∈ K }) x)
ext y
no goals
case h
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
K : LieSubalgebra R L
x y : { x // x ∈ K }
⊢ ↑(LinearMap.comp (↑(ad R L) ↑x) ↑(incl K)) y = ↑(LinearMap.comp (↑(incl K)) (↑(ad R { x // x ∈ K }) x)) y
simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp,
  LieSubalgebra.coe_bracket, Function.comp_apply]