no goals
G : Type u
inst✝¹ : Group G
N : Subgroup G
nN : Subgroup.Normal N
H : Type v
inst✝ : Group H
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z, z ∈ N ∧ x * z = y
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_prop, exists_eq_right]