simp_rw [QuotientGroup.preimage_image_mk_eq_iUnion_image N s, ← image_smul, Submonoid.smul_def,
  smul_eq_mul, mul_comm]
α : Type u_1
inst✝¹ : CommGroup α
N : Subgroup α
inst✝ : N.Normal
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ x, x • s
no goals