case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ Int.ofNat n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1

case negSucc
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ Int.negSucc n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d : G
n : ℤ
hn : n ≠ 0
x : G
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
cases' n with n n
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ ↑n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ Int.ofNat n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
simp only [Int.ofNat_eq_coe] at h
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ ↑n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
rw [zpow_ofNat] at h
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat n = 0
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
refine' ⟨n, Nat.pos_of_ne_zero fun n0 ↦ hn ?_, h⟩
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat 0 = 0
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat n = 0
rw [n0]
no goals
case ofNat
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.ofNat n ≠ 0
h : x ^ n = 1
n0 : n = 0
⊢ Int.ofNat 0 = 0
rfl
case negSucc
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ (n + 1) = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
case negSucc
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ Int.negSucc n = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
rw [zpow_negSucc, inv_eq_one] at h
no goals
case negSucc
α : Type ?u.63936
β : Type ?u.63939
G : Type u_1
inst✝ : Group G
a b c d x : G
n : ℕ
hn : Int.negSucc n ≠ 0
h : x ^ (n + 1) = 1
⊢ ∃ n, 0 < n ∧ x ^ n = 1
refine' ⟨n + 1, n.succ_pos, h⟩