rw [l1_2_20_ii' _ _ h]
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite ↑(Subgroup.closure {g})
G : Type u_1
inst✝ : Group G
g : G
h : ¬IsOfFinOrder g
⊢ Set.Infinite {x | ∃ i, g ^ i = x}