α : Type u_1
β : Type ?u.22286
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → Setoid.Rel s x y
α : Type u_1
β : Type ?u.22286
s : Setoid α
⊢ Subsingleton (Quotient s) ↔ s = ⊤
simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply,
  forall_const]
α : Type u_1
β : Type ?u.22286
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk s a = y) ↔ ∀ {y : α}, ⊤ → Setoid.Rel s a y
α : Type u_1
β : Type ?u.22286
s : Setoid α
⊢ (∀ (x y : Quotient s), x = y) ↔ ∀ {x y : α}, ⊤ → Setoid.Rel s x y
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun a => _)
α : Type u_1
β : Type ?u.22286
s : Setoid α
a b : α
⊢ Quotient.mk s a = Quotient.mk s b ↔ ⊤ → Setoid.Rel s a b
α : Type u_1
β : Type ?u.22286
s : Setoid α
a : α
⊢ (∀ (y : Quotient s), Quotient.mk s a = y) ↔ ∀ {y : α}, ⊤ → Setoid.Rel s a y
refine' (surjective_quotient_mk _).forall.trans (forall_congr' fun b => _)
α : Type u_1
β : Type ?u.22286
s : Setoid α
a b : α
⊢ Setoid.r a b ↔ Setoid.Rel s a b
α : Type u_1
β : Type ?u.22286
s : Setoid α
a b : α
⊢ Quotient.mk s a = Quotient.mk s b ↔ ⊤ → Setoid.Rel s a b
simp_rw [←Quotient.mk''_eq_mk, Prop.top_eq_true, true_implies, Quotient.eq'']
no goals
α : Type u_1
β : Type ?u.22286
s : Setoid α
a b : α
⊢ Setoid.r a b ↔ Setoid.Rel s a b
rfl