have ho : 0 < (orderOf x : ℤ) := by
  rwa [Int.coe_nat_pos, pos_iff_ne_zero, Ne.def, orderOf_eq_zero_iff, Classical.not_not]
case mp.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, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y
case mp.intro
G : Type u_1
inst✝ : Group G
x y : G
h : IsOfFinOrder x
i : ℤ
hi : (fun x_1 => x ^ x_1) i = y
ho : 0 < ↑(orderOf x)
⊢ ∃ n, 0 ≤ n ∧ n < ↑(orderOf x) ∧ x ^ n = y