G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
⊢ ∃ S, S ∈ leftTransversals ↑H ∧ g ∈ S
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_leftTransversals fun q => _,
    Quotient.mk'' g, Function.update_same (Quotient.mk'' g) g Quotient.out'⟩
case pos
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q

case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
by_cases hq : q = Quotient.mk'' g
no goals
case pos
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ ↑(Function.update Quotient.out' (Quotient.mk'' g) g q) = q
refine' (Function.update_noteq _ g Quotient.out') ▸ q.out_eq'
no goals
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : G ⧸ H
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g
exact hq