Theorem: QuotientGroup.preimage_image_mk_eq_iUnion_smul (LeanCamCombi/Mathlib/GroupTheory/QuotientGroup.lean)

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