no goals
k : Type u₁
G : Type u₂
R : Type ?u.399139
inst✝⁴ : Semiring k
α : Type u_1
β : Type u_2
α₂ : Type u_3
inst✝³ : Semiring β
inst✝² : One α
inst✝¹ : One α₂
F : Type u_4
inst✝ : OneHomClass F α α₂
f : F
⊢ mapDomain (↑f) 1 = 1
simp_rw [one_def, mapDomain_single, map_one]