case mk
α : Type u_1
β : Type ?u.5513
γ : Type ?u.5516
q : α × α
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝, snd✝) = Quotient.mk (Rel.setoid α) q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = Prod.swap q
α : Type u_1
β : Type ?u.5513
γ : Type ?u.5516
p q : α × α
⊢ Quotient.mk (Rel.setoid α) p = Quotient.mk (Rel.setoid α) q ↔ p = q ∨ p = Prod.swap q
cases p
case mk.mk
α : Type u_1
β : Type ?u.5513
γ : Type ?u.5516
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹) = Quotient.mk (Rel.setoid α) (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = Prod.swap (fst✝, snd✝)
case mk
α : Type u_1
β : Type ?u.5513
γ : Type ?u.5516
q : α × α
fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝, snd✝) = Quotient.mk (Rel.setoid α) q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = Prod.swap q
cases q
no goals
case mk.mk
α : Type u_1
β : Type ?u.5513
γ : Type ?u.5516
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ Quotient.mk (Rel.setoid α) (fst✝¹, snd✝¹) = Quotient.mk (Rel.setoid α) (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = Prod.swap (fst✝, snd✝)
simp only [eq_iff, Prod.mk.inj_iff, Prod.swap_prod_mk]