case intro.intro
G : Type u_1
H : Type ?u.170289
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g
G : Type u_1
H : Type ?u.170289
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
h : ExponentExists G
g : G
⊢ IsOfFinOrder g
obtain ⟨n, npos, hn⟩ := h
no goals
case intro.intro
G : Type u_1
H : Type ?u.170289
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
g : G
n : ℕ
npos : 0 < n
hn : ∀ (g : G), g ^ n = 1
⊢ IsOfFinOrder g
exact (isOfFinOrder_iff_pow_eq_one g).mpr ⟨n, npos, hn g⟩