case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ (x : { x // x ∈ N }), (fun y => y * ↑x) ⁻¹' s
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ (x : { x // x ∈ N }), (fun y => y * ↑x) ⁻¹' s
ext x
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N) ↔ ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ (x : { x // x ∈ N }), (fun y => y * ↑x) ⁻¹' s
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
  Set.mem_image, ← eq_inv_mul_iff_mul_eq]
no goals
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N) ↔ ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
exact
  ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ =>
    ⟨x * z, hxz, by simpa using hz⟩⟩
no goals
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s
simpa using hs
no goals
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N
simpa using hz