case h.e'_5
α : Type u_1
β : Type ?u.35146
γ : Type ?u.35149
a : α
z : Sym2 α
h : a ∈ z
⊢ z = Quotient.mk (Rel.setoid α) (a, Mem.other h)
α : Type u_1
β : Type ?u.35146
γ : Type ?u.35149
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h ∈ z
convert mem_mk''_right a <| Mem.other h
no goals
case h.e'_5
α : Type u_1
β : Type ?u.35146
γ : Type ?u.35149
a : α
z : Sym2 α
h : a ∈ z
⊢ z = Quotient.mk (Rel.setoid α) (a, Mem.other h)
rw [other_spec h]