α : Type u_1
β : Type ?u.4046
γ : Type ?u.4049
a b : α
⊢ (a, b) ≈ (b, a)
α : Type u_1
β : Type ?u.4046
γ : Type ?u.4049
a b : α
⊢ Quotient.mk (Rel.setoid α) (a, b) = Quotient.mk (Rel.setoid α) (b, a)
rw [Quotient.eq]
no goals
α : Type u_1
β : Type ?u.4046
γ : Type ?u.4049
a b : α
⊢ (a, b) ≈ (b, a)
apply Rel.swap