case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x⁻¹ ^ n = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
x : G
hx : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ x⁻¹ ^ n = 1
rcases(isOfFinOrder_iff_pow_eq_one x).mp hx with ⟨n, npos, hn⟩
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
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ x⁻¹ ^ n = 1
refine' ⟨n, npos, by simp_rw [inv_pow, hn, inv_one]⟩
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
x : G
hx : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ x⁻¹ ^ n = 1
simp_rw [inv_pow, hn, inv_one]