G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ S ∈ leftTransversals ↑H ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
simp_rw [mem_leftTransversals_iff_existsUnique_inv_mul_mem, SetLike.mem_coe, ←
  QuotientGroup.eq']
no goals
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
⊢ (∀ (g : G), ∃! s, ↑↑s = ↑g) ↔ ∀ (q : Quotient (QuotientGroup.leftRel H)), ∃! s, Quotient.mk'' ↑s = q
exact ⟨fun h q => Quotient.inductionOn' q h, fun h g => h (Quotient.mk'' g)⟩