no goals
k : Type u_2
G : Type u_3
V : Type u_1
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(↑(asGroupHom ρ) g) = ↑ρ g
simp only [asGroupHom, MonoidHom.coe_toHomUnits]