p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
h : H
g : G
hg : ↑ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1
p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
⊢ IsPGroup p H
refine' fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => _) (hG g)
no goals
p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
h : H
g : G
hg : ↑ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]