use n
case intro
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ ∃ i, g ^ i = x
case h
G : Type u_1
inst✝ : Group G
g : G
h : orderOf g = 0
this : Set.Infinite ((fun i => g ^ i) '' Set.univ)
x : G
n : ℕ
hn : g ^ n = x
⊢ g ^ ↑n = x