case mk
α : Type u_1
β : Type ?u.4166
γ : Type ?u.4169
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap (fst✝, snd✝)) = Quotient.mk (Rel.setoid α) (fst✝, snd✝)
α : Type u_1
β : Type ?u.4166
γ : Type ?u.4169
p : α × α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap p) = Quotient.mk (Rel.setoid α) p
cases p
no goals
case mk
α : Type u_1
β : Type ?u.4166
γ : Type ?u.4169
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (Prod.swap (fst✝, snd✝)) = Quotient.mk (Rel.setoid α) (fst✝, snd✝)
exact eq_swap