case h
α : Type ?u.21855
G : Type u_1
A : Type ?u.21861
S : Type ?u.21864
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x : G
⊢ x ∈ s * ↑N ↔ x ∈ ↑N * s
α : Type ?u.21855
G : Type u_1
A : Type ?u.21861
S : Type ?u.21864
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
⊢ s * ↑N = ↑N * s
ext x
case h
α : Type ?u.21855
G : Type u_1
A : Type ?u.21861
S : Type ?u.21864
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x y : G
⊢ (∃ b, y ∈ s ∧ b ∈ ↑N ∧ (fun x x_1 => x * x_1) y b = x) ↔ ∃ y_1, y_1 ∈ ↑N ∧ y ∈ s ∧ (fun x x_1 => x * x_1) y_1 y = x
case h
α : Type ?u.21855
G : Type u_1
A : Type ?u.21861
S : Type ?u.21864
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x : G
⊢ x ∈ s * ↑N ↔ x ∈ ↑N * s
refine (exists_congr fun y => ?_).trans exists_swap
no goals
case h
α : Type ?u.21855
G : Type u_1
A : Type ?u.21861
S : Type ?u.21864
inst✝¹ : Group G
inst✝ : AddGroup A
s✝ s : Set G
N : Subgroup G
hN : Normal N
x y : G
⊢ (∃ b, y ∈ s ∧ b ∈ ↑N ∧ (fun x x_1 => x * x_1) y b = x) ↔ ∃ y_1, y_1 ∈ ↑N ∧ y ∈ s ∧ (fun x x_1 => x * x_1) y_1 y = x
simp only [exists_and_left, @and_left_comm _ (y ∈ s), ← eq_inv_mul_iff_mul_eq (b := y),
  ← eq_mul_inv_iff_mul_eq  (c := y), exists_eq_right, SetLike.mem_coe, hN.mem_comm_iff]