no goals
k : Type u₁
G : Type u₂
R : Type ?u.2773678
A : Type u_1
H : Type u_2
F : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Semiring A
inst✝³ : Algebra k A
inst✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddMonoidHomClass F G H
f : F
r : k
⊢ mapDomain (↑f) (↑(algebraMap k (AddMonoidAlgebra A G)) r) = ↑(algebraMap k (AddMonoidAlgebra A H)) r
simp only [Function.comp_apply, mapDomain_single, AddMonoidAlgebra.coe_algebraMap, map_zero]