G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H.toSubmonoid ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Quotient ↑H.toSubmonoid ↑⊥ = _root_.Quotient (QuotientGroup.rightRel H)
unfold Quotient
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑H.toSubmonoid ↑⊥ = QuotientGroup.rightRel H
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H.toSubmonoid ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)
congr
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.rightRel H) a✝ b✝
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑H.toSubmonoid ↑⊥ = QuotientGroup.rightRel H
ext
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (setoid ↑H ↑⊥) a✝ b✝
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.rightRel H) a✝ b✝
simp_rw [← rel_bot_eq_right_group_rel H]
no goals
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type ?u.70749
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (setoid ↑H ↑⊥) a✝ b✝
rfl