simp only [Cardinal.mk_fintype, Nat.cast_inj, Fintype.card_ofFinset]
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑((fun i => g ^ i) '' Set.Ico 0 (orderOf g)) = ↑(orderOf g)
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Finset.image (fun i => g ^ i) (Set.toFinset (Set.Ico 0 (orderOf g)))).card = orderOf g