α : Type u_1
β : Type ?u.6005
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → Rel s x y) ↔ ∀ (x y : α), Rel s x y
α : Type u_1
β : Type ?u.6005
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), Rel s x y
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]
no goals
α : Type u_1
β : Type ?u.6005
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → Rel s x y) ↔ ∀ (x y : α), Rel s x y
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]