{A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A. Proof. snrapply Build_NormalSubgroup. - srapply (Build_Subgroup' (fun x => f x = group_unit)); cbn beta. 1: apply grp_homo_unit. intros x y p q. apply (grp_homo_moveL_1M _ _ _)^-1. exact (p @ q^). - intros x y; cbn; intros p. apply (grp_homo_moveL_1V _ _ _)^-1. lhs_V nrapply grp_inv_inv. apply (ap (-)). exact ((grp_homo_moveL_1V f x y) p)^. Defined.
Require Import Basics Types. Require Import Algebra.Groups.Group. Require Import Algebra.Groups.Subgroup. Require Import WildCat.Core.