p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ ∀ (g : H), ∃ k, ↑ϕ g ^ p ^ k = 1
p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ IsPGroup p H
simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
no goals
p : ℕ
G : Type u_2
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_1
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ ∀ (g : H), ∃ k, ↑ϕ g ^ p ^ k = 1
exact fun h => hG (ϕ h)