rw [l1_2_20_i' _ _ h]
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑↑(Subgroup.closure {g}) = ↑(orderOf g)
G : Type u_1
inst✝ : Group G
g : G
h : IsOfFinOrder g
this : orderOf g ≠ 0
⊢ #↑{x | ∃ i ∈ Set.Ico 0 (orderOf g), g ^ i = x} = ↑(orderOf g)