no goals
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
classical
rw [other_eq_other'] at hb⊢
convert other_invol' ha hb using 2
apply other_eq_other'
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb : Mem.other ha ∈ z
⊢ Mem.other hb = a
rw [other_eq_other'] at hb⊢
case h.e'_2.h.e'_3
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other' hb✝ = a
convert other_invol' ha hb using 2
no goals
case h.e'_2.h.e'_3
α : Type u_1
β : Type ?u.114502
γ : Type ?u.114505
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha
apply other_eq_other'