no goals
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
φ : G →* H
a✝ b✝ : G ⧸ ker φ
a b : G
h : ↑φ a = ↑φ b
⊢ Setoid.r a b
rw [leftRel_apply, mem_ker, φ.map_mul, ← h, φ.map_inv, inv_mul_self]