M : Type u_1
A : Type ?u.55052
B : Type ?u.55055
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ↑(↑(powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
M : Type u_1
A : Type ?u.55052
B : Type ?u.55055
inst✝ : Monoid M
x y : M
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y
rw [closure_singleton_eq, mem_mrange]
no goals
M : Type u_1
A : Type ?u.55052
B : Type ?u.55055
inst✝ : Monoid M
x y : M
⊢ (∃ x_1, ↑(↑(powersHom M) x) x_1 = y) ↔ ∃ n, x ^ n = y
rfl