no goals
M : Type u_3
A : Type ?u.225218
B : Type ?u.225221
inst✝² : Monoid M
N : Type u_1
F : Type u_2
inst✝¹ : Monoid N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (↑f m)
simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]