case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
⊢ (x ^ i) ^ orderOf x = 1
by_cases h : IsOfFinOrder x
no goals
case pos
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
rw [← zpow_ofNat, ← zpow_mul, mul_comm, zpow_mul, zpow_ofNat, pow_orderOf_eq_one, one_zpow]
no goals
case neg
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
rw [orderOf_eq_zero h, _root_.pow_zero]