refine' ⟨n.natAbs, _, _⟩
case intro.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ ∃ n < orderOf x, x ^ n = y
case intro.intro.intro.refine'_1
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ Int.natAbs n < orderOf x

case intro.intro.intro.refine'_2
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
n : ℤ
hnonneg : 0 ≤ n
hlt : n < ↑(orderOf x)
heq : x ^ n = y
⊢ x ^ Int.natAbs n = y