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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ ↑(lift R).symm g = f
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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑g ∘ ↑(ι R) = ↑f ↔ g = ↑(lift R) f
refine' Iff.trans _ (lift R).symm_apply_eq
case mpr
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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
⊢ ↑g ∘ ↑(ι R) = ↑f
case mpr
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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
⊢ ↑(lift R).symm g = f → ↑g ∘ ↑(ι R) = ↑f
intro h
case mpr.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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
x✝ : L
⊢ (↑g ∘ ↑(ι R)) x✝ = ↑f x✝
case mpr
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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
⊢ ↑g ∘ ↑(ι R) = ↑f
ext
no goals
case mpr.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 : UniversalEnvelopingAlgebra R L →ₐ[R] A
h : ↑(lift R).symm g = f
x✝ : L
⊢ (↑g ∘ ↑(ι R)) x✝ = ↑f x✝
simp [← h]