apply Iff.intro
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) ↔ injective (group_homomorphism.fn G H)
case mp
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ set_eq (kernel G H hom) (trivial_subgroup G) → injective (group_homomorphism.fn G H)

case mpr
α : Type u_1
β : Type u_2
G : group α
H : group β
hom : group_homomorphism G H
φ : α → β := group_homomorphism.fn G H
hphi : φ = group_homomorphism.fn G H
⊢ injective (group_homomorphism.fn G H) → set_eq (kernel G H hom) (trivial_subgroup G)