p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H) }
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ H ⊔ K }
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' K) }
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H) }
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
no goals
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' K) }
rwa [QuotientGroup.ker_mk']