α : Type u_1
β : Type ?u.105502
γ : Type ?u.105505
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
α : Type u_1
β : Type ?u.105502
γ : Type ?u.105505
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other' h ∈ z
rw [← other_eq_other']
no goals
α : Type u_1
β : Type ?u.105502
γ : Type ?u.105505
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
exact other_mem h