case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ ∃ i x_1, x ^ i = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
⊢ ∃ i x_1, x ^ i = 1
rcases exists_pow_eq_one x with ⟨w, hw1, hw2⟩
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ ↑w = 1
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ ∃ i x_1, x ^ i = 1
refine' ⟨w, Int.coe_nat_ne_zero.mpr (_root_.ne_of_gt hw1), _⟩
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ w = 1
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ ↑w = 1
rw [zpow_ofNat]
no goals
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Group G
inst✝¹ : AddGroup A
inst✝ : Finite G
x : G
w : ℕ
hw1 : w > 0
hw2 : IsPeriodicPt ((fun x x_1 => x * x_1) x) w 1
⊢ x ^ w = 1
exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2