no goals
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : { x // x ∈ ker f } →* A), comp f u = comp f v → u = v
⊢ ker f = ⊥
simpa using _root_.congr_arg range (h f.ker.subtype 1 (by aesop_cat))
no goals
A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : { x // x ∈ ker f } →* A), comp f u = comp f v → u = v
⊢ comp f (Subgroup.subtype (ker f)) = comp f 1
aesop_cat