no goals
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type ?u.547902
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (FreeAlgebra R X)) x) = x
simp [algebraMapInv]