no goals
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
f : X → L
x : X
⊢ ↑(↑(lift R) f) (of R x) = f x
rw [← @Function.comp_apply  _ _ _ (lift R f) (of R) x, of_comp_lift]