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 : ↑(rangeRestrict φ) a = ↑(rangeRestrict φ) b
⊢ Setoid.r a b
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
  φ.rangeRestrict.map_inv, inv_mul_self]