case h
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), ↑F₁ (of R x) = ↑F₂ (of R x)
x✝ : X
⊢ ↑(lift R).symm F₁ x✝ = ↑(lift R).symm F₂ x✝
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), ↑F₁ (of R x) = ↑F₂ (of R x)
⊢ ↑(lift R).symm F₁ = ↑(lift R).symm F₂
ext
no goals
case h
R : Type u
X : Type v
inst✝² : CommRing R
L : Type w
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L
h : ∀ (x : X), ↑F₁ (of R x) = ↑F₂ (of R x)
x✝ : X
⊢ ↑(lift R).symm F₁ x✝ = ↑(lift R).symm F₂ x✝
simp [h]