α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ (∀ (b : α), b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s
rw [← mem_sym2_iff]
no goals
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a b : α
m : Sym2 α
⊢ Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
exact mk'_mem_sym2_iff.trans <| and_self_iff _