no goals
G : Type u_1
G' : Type ?u.530012
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.530021
inst✝³ : AddGroup A
N : Type ?u.530027
P : Type ?u.530030
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_2
inst✝ : MulOneClass M
f : G →* M
h : ker f = ⊥
x y : G
hxy : ↑f x = ↑f y
⊢ x = y
rwa [eq_iff, h, mem_bot, inv_mul_eq_one, eq_comm] at hxy