G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (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 ∈ rightTransversals ↑H ∧ g ∈ S
refine'
  ⟨Set.range (Function.update Quotient.out' _ g), range_mem_rightTransversals 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 : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (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 : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (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 : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (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 : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (Function.update Quotient.out' (Quotient.mk'' g) g q) = q
exact hq.symm ▸ congr_arg _ (Function.update_same (Quotient.mk'' g) g Quotient.out')
no goals
case neg
G : Type u_1
inst✝ : Group G
H K : Subgroup G
S T : Set G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (Function.update Quotient.out' (Quotient.mk'' g) g q) = q
exact Eq.trans (congr_arg _ (Function.update_noteq hq g Quotient.out')) q.out_eq'