case h
α : Type u_1
β : Type ?u.101059
γ : Type ?u.101062
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
α : Type u_1
β : Type ?u.101059
γ : Type ?u.101062
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = z
induction z using Sym2.ind
case h
α : Type u_1
β : Type ?u.101059
γ : Type ?u.101062
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
case h
α : Type u_1
β : Type ?u.101059
γ : Type ?u.101062
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
have h' := mem_iff.mp h
no goals
case h
α : Type u_1
β : Type ?u.101059
γ : Type ?u.101062
inst✝ : DecidableEq α
a x✝ y✝ : α
h : a ∈ Quotient.mk (Rel.setoid α) (x✝, y✝)
h' : a = x✝ ∨ a = y✝
⊢ Quotient.mk (Rel.setoid α) (a, Mem.other' h) = Quotient.mk (Rel.setoid α) (x✝, y✝)
aesop (add norm unfold [Quotient.rec, Quot.rec]) (rule_sets [Sym2])