no goals
R : Type u_2
A : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
e : { e // e * e = 0 }
⊢ ↑(↑lift e) ε = ↑e
simp only [lift_apply_apply, fst_eps, map_zero, snd_eps, one_smul, zero_add]