case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder h
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
⊢ IsOfFinOrder h
obtain ⟨g, hg⟩ := hf h
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder (↑f g)
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder h
rw [← hg]
no goals
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
N : Subgroup G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ↑f
tG : IsTorsion G
h : H
g : G
hg : ↑f g = h
⊢ IsOfFinOrder (↑f g)
exact f.isOfFinOrder (tG g)