no goals
G : Type u_1
G' : Type ?u.556305
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.556314
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
H : Subgroup G
f : G →* N
hf : Injective ↑f
⊢ map f H = ⊥ ↔ H = ⊥
rw [map_eq_bot_iff, f.ker_eq_bot_iff.mpr hf, le_bot_iff]