simp only [tsub_zero, eq_self_iff_true, Set.toFinset_card, Nat.card_fintypeIco]
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ (Set.toFinset (Set.Ico 0 (orderOf g))).card = orderOf g

G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ Set.InjOn (fun i => g ^ i) ↑(Set.toFinset (Set.Ico 0 (orderOf g)))