no goals
k : Type u₁
G : Type u₂
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Semiring k
inst✝¹ : One G
g_hom : Type u_1
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ ↑(liftNC ↑f ↑g) 1 = 1
simp [one_def]