case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type v
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ ↑f x ^ n = 1
G : Type u
A : Type v
x✝ y : G
a b : A
n m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type v
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
⊢ ∃ n, 0 < n ∧ ↑f x ^ n = 1
rcases(isOfFinOrder_iff_pow_eq_one _).mp h with ⟨n, npos, hn⟩
no goals
case intro.intro
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type v
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ∃ n, 0 < n ∧ ↑f x ^ n = 1
exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩
no goals
G : Type u
A : Type v
x✝ y : G
a b : A
n✝ m : ℕ
inst✝² : Monoid G
inst✝¹ : AddMonoid A
H : Type v
inst✝ : Monoid H
f : G →* H
x : G
h : IsOfFinOrder x
n : ℕ
npos : 0 < n
hn : x ^ n = 1
⊢ ↑f x ^ n = 1
rw [← f.map_pow, hn, f.map_one]