case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
x✝ : L
⊢ ↑(↑(lift R).symm g₁) x✝ = ↑(↑(lift R).symm g₂) x✝
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
⊢ ↑(lift R).symm g₁ = ↑(lift R).symm g₂
ext
no goals
case h
R : Type u₁
L : Type u₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
A : Type u₃
inst✝¹ : Ring A
inst✝ : Algebra R A
f : L →ₗ⁅R⁆ A
g₁ g₂ : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : LieHom.comp (AlgHom.toLieHom g₁) (ι R) = LieHom.comp (AlgHom.toLieHom g₂) (ι R)
x✝ : L
⊢ ↑(↑(lift R).symm g₁) x✝ = ↑(↑(lift R).symm g₂) x✝
simp [h]