p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ MonoidHom.range (MonoidHom.comp ϕ (Subgroup.subtype H)) }
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ Subgroup.map ϕ H }
rw [← H.subtype_range, MonoidHom.map_range]
no goals
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ MonoidHom.range (MonoidHom.comp ϕ (Subgroup.subtype H)) }
exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective