no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type u_1
inst✝ : Monoid H
f : G →* H
hf : Injective ↑f
x : G
⊢ orderOf (↑f x) = orderOf x
simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]