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