R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ↑f ∘ ι R = ↑g ∘ ι R
⊢ f = g
rw [← lift_symm_apply, ← lift_symm_apply] at w
no goals
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
exact (lift R).symm.injective w