case intro
G : Type u
A : Type v
x : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
h : y ∈ Subgroup.zpowers x
⊢ orderOf y ∣ orderOf x
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
case intro
G : Type u
A : Type v
x : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ (x ^ k) ^ orderOf x = 1
case intro
G : Type u
A : Type v
x : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ orderOf (x ^ k) ∣ orderOf x
rw [orderOf_dvd_iff_pow_eq_one]
no goals
case intro
G : Type u
A : Type v
x : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i k : ℤ
h : x ^ k ∈ Subgroup.zpowers x
⊢ (x ^ k) ^ orderOf x = 1
exact zpow_pow_orderOf